:: The Jordan's Property for Certain Subsets of the Plane
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PRE_TOPC, REAL_1, CARD_1, XXREAL_1, XXREAL_0,
FUNCT_1, BORSUK_1, ORDINAL2, RELAT_2, RELAT_1, SUBSET_1, FUNCOP_1,
CONNSP_1, EUCLID, RLVECT_1, CONVEX1, RLTOPSP1, TARSKI, TOPREAL1, TOPS_2,
STRUCT_0, ARYTM_3, MCART_1, ARYTM_1, PCOMPS_1, RCOMP_1, METRIC_1,
SQUARE_1, JORDAN1, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, NUMBERS, PRE_TOPC, TOPS_2,
CONNSP_1, SQUARE_1, RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1,
TOPREAL1, RLVECT_1, RLTOPSP1, EUCLID;
constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPMETR, TOPREAL1,
FUNCOP_1, FUNCSDOM, CONVEX1, BINOP_2, PCOMPS_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, STRUCT_0,
PRE_TOPC, BORSUK_1, EUCLID, RLTOPSP1, SQUARE_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, CONNSP_1, XBOOLE_0;
equalities EUCLID, SQUARE_1, SUBSET_1, STRUCT_0, PCOMPS_1, RLTOPSP1;
expansions TARSKI, CONNSP_1, XBOOLE_0;
theorems TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2, SUBSET_1, RCOMP_1, METRIC_1,
PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, CONNSP_1, SQUARE_1, TOPMETR,
TOPREAL1, EUCLID, TOPREAL3, TREAL_1, XBOOLE_0, XBOOLE_1, XREAL_1,
ZFMISC_1, SPPOL_1, XXREAL_0, RLTOPSP1;
begin
::
:: Selected theorems on connected space
::
reserve GX,GY for non empty TopSpace,
x,y for Point of GX,
r,s for Real;
Lm1: 0 in [.0,1.] & 1 in [.0,1.]
proof
A1: 0 in {r:0<=r & r<=1};
1 in {s:0<=s & s<=1};
hence thesis by A1,RCOMP_1:def 1;
end;
theorem Th1: ::Arcwise connectedness derives connectedness
for GX being non empty TopSpace st (for x,y being Point of GX
ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1)
holds GX is connected
proof
let GX;
assume
A1: for x,y being Point of GX
ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1;
for x,y being Point of GX ex GY st (GY is connected &
ex f being Function of GY,GX st f is continuous & x in rng(f)& y in rng(f))
proof
let x,y;
now
consider h being Function of I[01],GX such that
A2: h is continuous and
A3: x=h.0 and
A4: y=h.1 by A1;
A5: 0 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A6: 1 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A7: x in rng h by A3,A5,FUNCT_1:def 3;
y in rng h by A4,A6,FUNCT_1:def 3;
hence thesis by A2,A7,TREAL_1:19;
end;
hence thesis;
end;
hence thesis by TOPS_2:63;
end;
theorem Th2: ::Arcwise connectedness derives connectedness for subset
for A being Subset of GX st
(for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1)
holds A is connected
proof
let A be Subset of GX;
assume that
A1: for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1;
per cases;
suppose A is non empty;
then reconsider A as non empty Subset of GX;
A2: for xa,ya being Point of GX st xa in A & ya in A & xa = ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1
proof
let xa,ya be Point of GX;
assume that
A3: xa in A and ya in A and
A4: xa = ya;
reconsider xa9 = xa as Element of GX|A by A3,PRE_TOPC:8;
reconsider h = I[01] --> xa9 as Function of I[01], GX|A;
take h;
thus thesis by A4,Lm1,BORSUK_1:40,FUNCOP_1:7;
end;
for xb,yb being Point of GX|A
ex ha being Function of I[01],GX|A st ha is continuous & xb=ha.0 & yb=ha.1
proof
let xb,yb be Point of GX|A;
A5: xb in [#](GX|A);
A6: yb in [#](GX|A);
A7: xb in A by A5,PRE_TOPC:def 5;
A8: yb in A by A6,PRE_TOPC:def 5;
per cases;
suppose xb<>yb;
hence thesis by A1,A7,A8;
end;
suppose xb = yb;
hence thesis by A2,A7;
end;
end;
then GX|A is connected by Th1;
hence thesis;
end;
suppose A is empty;
then reconsider D = A as empty Subset of GX;
let A1, B1 be Subset of GX|A such that
[#](GX|A) = A1 \/ B1 and A1,B1 are_separated;
[#](GX|D) = D;
hence thesis;
end;
end;
theorem
for A0 being Subset of GX, A1 being Subset of GX st
A0 is connected & A1 is connected & A0 meets A1
holds A0 \/ A1 is connected by CONNSP_1:1,17;
theorem Th4:
for A0,A1,A2 being Subset of GX st
A0 is connected & A1 is connected & A2 is connected & A0 meets A1 &
A1 meets A2 holds A0 \/ A1 \/ A2 is connected
proof
let A0,A1,A2 be Subset of GX;
assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A0 meets A1 and
A5: A1 meets A2;
A6: A1 /\ A2 <> {} by A5;
A7: A0 \/ A1 is connected by A1,A2,A4,CONNSP_1:1,17;
(A0 \/ A1)/\ A2= A0 /\ A2 \/ A1 /\ A2 by XBOOLE_1:23;
then (A0 \/ A1) meets A2 by A6;
hence thesis by A3,A7,CONNSP_1:1,17;
end;
theorem Th5:
for A0,A1,A2,A3 being Subset of GX st A0 is connected & A1 is connected &
A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 &
A2 meets A3 holds A0 \/ A1 \/ A2 \/ A3 is connected
proof
let A0,A1,A2,A3 be Subset of GX;
assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A3 is connected and
A5: A0 meets A1 and
A6: A1 meets A2 and
A7: A2 meets A3;
A8: A2 /\ A3 <> {} by A7;
A9: A0 \/ A1 \/ A2 is connected by A1,A2,A3,A5,A6,Th4;
(A0 \/ A1 \/ A2)/\ A3= (A0 \/ A1) /\ A3 \/ A2 /\ A3 by XBOOLE_1:23;
then (A0 \/ A1 \/ A2) meets A3 by A8;
hence thesis by A4,A9,CONNSP_1:1,17;
end;
begin
::
:: Certain connected and open subsets in the Euclidean plane
::
reserve Q,P1,P2 for Subset of TOP-REAL 2;
reserve P for Subset of TOP-REAL 2;
reserve w1,w2 for Point of TOP-REAL 2;
definition
let V be RealLinearSpace, P be Subset of V;
redefine attr P is convex means
for w1,w2 being Element of V st w1 in P & w2 in P holds LSeg(w1,w2) c= P;
compatibility by RLTOPSP1:22;
end;
registration let n be Nat;
cluster convex -> connected for Subset of TOP-REAL n;
coherence
proof
let P be Subset of TOP-REAL n;
assume that
A1: for w3,w4 being Point of TOP-REAL n st w3 in P & w4 in P holds
LSeg(w3,w4) c= P;
for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P & w1<>w2
ex h being Function of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w2=h.1
proof
let w1,w2 be Point of TOP-REAL n;
assume that
A2: w1 in P and
A3: w2 in P and
A4: w1<>w2;
A5: LSeg(w1,w2) c= P by A1,A2,A3;
LSeg(w1,w2) is_an_arc_of w1,w2 by A4,TOPREAL1:9;
then consider f being Function of I[01], (TOP-REAL n)|LSeg(w1,w2) such that
A6: f is being_homeomorphism and
A7: f.0 = w1 and
A8: f.1 = w2 by TOPREAL1:def 1;
A9: f is continuous by A6,TOPS_2:def 5;
A10: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A6,TOPS_2:def 5;
then
A11: rng f c= P by A5,PRE_TOPC:def 5;
then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
by A10,PRE_TOPC:def 5;
then
A12: (TOP-REAL n)|LSeg(w1,w2) is SubSpace of (TOP-REAL n)|P by TOPMETR:3;
dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider g=f as Function of [.0,1.],P by A11,FUNCT_2:2;
the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P)
.= P by PRE_TOPC:def 5;
then reconsider gt=g as Function of I[01],(TOP-REAL n)|P by BORSUK_1:40;
gt is continuous by A9,A12,PRE_TOPC:26;
hence thesis by A7,A8;
end;
hence thesis by Th2;
end;
end;
reserve pa,pb for Point of TOP-REAL 2,
s1,t1,s2,t2,s,t,s3,t3,s4,t4,s5,t5,s6,t6, l,sa,sd,ta,td for Real;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;
Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
Lm3: for s1 holds { |[ sb,tb ]|:sb w`1 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th11:
for t1,P st P = {|[ s,t ]|:t1 w`2 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th13:
for s1,t1,s2,t2,P st P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
holds P is connected
proof
let s1,t1,s2,t2,P;
assume P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
then
A1: P={ |[ s3,t3 ]|:s3 {} by A4,XBOOLE_0:def 4;
then
A5: A0 meets A1;
A6: s2< s2+1 by XREAL_1:29;
A7: |[s2+1,t1-1]| in A1 by A3;
|[s2+1,t1-1]| in A2 by A6;
then A1 /\ A2 <> {} by A7,XBOOLE_0:def 4;
then
A8: A1 meets A2;
A9: t2< t2+1 by XREAL_1:29;
A10: |[s2+1,t2+1]| in A2 by A6;
|[s2+1,t2+1]| in A3 by A9;
then A2 /\ A3 <> {} by A10,XBOOLE_0:def 4;
then
A11: A2 meets A3;
A12: A0 is convex by Th10;
A13: A1 is convex by Th12;
A14: A2 is convex by Th9;
A3 is convex by Th11;
hence thesis by A1,A5,A8,A11,A12,A13,A14,Th5;
end;
Lm9: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
theorem Th14:
for s1 holds { |[ s,t ]|:s1~~0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1~~~~0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)s } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1>s } as Subset of REAL 2 by Lm3;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real st
r>0 & Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1>s;
set r=(s1-s)/2;
A3: s1-s>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q) pq`1 by XREAL_1:19;
then
A11: s+(s1-s)/2 > pq`1 by A1,EUCLID:52;
s+(s1-s)/2 =s1-r;
then
A12: s1> s+(s1-s)/2 by A3,XREAL_1:44,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1>pq`1 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th16:
for s1 holds { |[ s,t ]|:s10 & Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s10 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)t } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1>t } as Subset of REAL 2 by Lm4;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real st r>0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1>t;
set r=(s1-t)/2;
A3: s1-t>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q) pq`2 by XREAL_1:19;
then
A11: t+(s1-t)/2 > pq`2 by A1,EUCLID:52;
t+(s1-t)/2 =s1-r;
then
A12: s1> t+(s1-t)/2 by A3,XREAL_1:44,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1>pq`2 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th18:
for s1,t1,s2,t2 holds
{ |[ s,t ]|:s1~~~~= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1 {} & P1 misses P2 &
for P1A,P2B being Subset of (TOP-REAL 2)|P` st P1A = P1 & P2B = P2 holds
P1A is a_component & P2B is a_component
proof
let s1,t1,s2,t2;
let P,P1,P2 be Subset of TOP-REAL 2;
assume that
A1: s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or
pd`1 <= s2 & pd`1 >= s1 & pd`2 = t2 or
pd`1 <= s2 & pd`1 >= s1 & pd`2 = t1 or
pd`1 = s2 & pd`2 <= t2 & pd`2 >= t1)by A3,A7;
then s1= t1 or
pb`1 <= s2 & pb`1 >= s1 & pb`2 = t2 or
pb`1 <= s2 & pb`1 >= s1 & pb`2 = t1 or
pb`1 = s2 & pb`2 <= t2 & pb`2 >= t1) by A3;
hence contradiction by A11;
end;
hence x in P` by A10,SUBSET_1:29;
end;
suppose x in P2;
then consider pc being Point of TOP-REAL 2 such that
A12: pc=x and
A13: not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2) by A5;
now
assume pc in P;
then ex p being Point of TOP-REAL 2 st p=pc & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1) by A3;
hence contradiction by A1,A2,A13;
end;
hence x in P`by A12,SUBSET_1:29;
end;
end;
hence x in P`;
end;
then
A14: P1 \/ P2 c= P`;
hence
A15: P`=P1 \/ P2 by A8;
set s3 =(s1+s2)/2, t3=(t1+t2)/2;
A16: s1+s1{} by A4,A14;
set P9 = P`;
P1 misses P2 by A4,A5,Th29;
hence
A26: P1 /\ P2 = {};
now
let P1A,P2B be Subset of (TOP-REAL 2)|P9;
assume that
A27: P1A=P1 and
A28: P2B=P2;
P1 is convex by A4,Th25;
then
A29: P1A is connected by A27,CONNSP_1:23;
A30: P2 is connected by A5,Th26;
A31: P2={ |[ sa,ta ]|:not (s1<=sa & sa<=s2 & t1<=ta & ta<=t2)} by A5,Th22;
reconsider A0={ |[ s3a,t3a ]|:s3at2 by XREAL_1:29;
then
A33: |[s2+1,t2+1]| in A3;
A34: P2B is connected by A28,A30,CONNSP_1:23;
A35: for CP being Subset of (TOP-REAL 2)|(P9) st
CP is connected holds P1A c= CP implies P1A = CP
proof
let CP be Subset of (TOP-REAL 2)|(P9);
assume CP is connected;
then
A36: ((TOP-REAL 2)|P9)|CP is connected;
now
assume
A37: P1A c= CP;
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A38: P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
P1 is open by A4,Th27;
then
A39: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A40: P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A38,PRE_TOPC:def 5;
then
A41: P1A in the topology of (TOP-REAL 2)|P9 by A39,PRE_TOPC:def 4;
A42: CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A43: AP<>{}(((TOP-REAL 2)|P9)|CP) by A4,A25,A27,A37,XBOOLE_1:28;
AP in the topology of ((TOP-REAL 2)|P9)|CP by A41,A42,PRE_TOPC:def 4;
then
A44: AP is open by PRE_TOPC:def 2;
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A45: P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
P2 is open by A5,Th28;
then
A46: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A45,PRE_TOPC:def 5;
then
A47: P2B in the topology of (TOP-REAL 2)|P9 by A46,PRE_TOPC:def 4;
CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
then BP in the topology of ((TOP-REAL 2)|P9)|CP by A47,PRE_TOPC:def 4;
then
A48: BP is open by PRE_TOPC:def 2;
A49: CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A40,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now
assume
A50: BP<>{};
A51: AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
.= P1A /\ P2B /\ CP;
P1 misses P2 by A4,A5,Th29;
then P1 /\ P2 = {};
then AP misses BP by A27,A28,A51;
hence contradiction by A36,A42,A43,A44,A48,A49,A50,CONNSP_1:11;
end;
hence thesis by A49,XBOOLE_1:28;
end;
hence thesis;
end;
hence P1A is a_component by A29;
for CP being Subset of (TOP-REAL 2)|(P9) st
CP is connected holds P2B c= CP implies P2B = CP
proof
let CP be Subset of (TOP-REAL 2)|(P9);
assume CP is connected;
then
A52: ((TOP-REAL 2)|P9)|CP is connected;
assume
A53: P2B c= CP;
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A54: P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
P2 is open by A5,Th28;
then
A55: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A56: P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A54,PRE_TOPC:def 5;
then
A57: P2B in the topology of (TOP-REAL 2)|P9 by A55,PRE_TOPC:def 4;
A58: CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A59: BP<>{}(((TOP-REAL 2)|P9)|CP) by A28,A32,A33,A53,XBOOLE_1:28;
BP in the topology of ((TOP-REAL 2)|P9)|CP by A57,A58,PRE_TOPC:def 4;
then
A60: BP is open by PRE_TOPC:def 2;
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A61: P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
P1 is open by A4,Th27;
then
A62: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A61,PRE_TOPC:def 5;
then
A63: P1A in the topology of (TOP-REAL 2)|P9 by A62,PRE_TOPC:def 4;
CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
then AP in the topology of ((TOP-REAL 2)|P9)|CP by A63,PRE_TOPC:def 4;
then
A64: AP is open by PRE_TOPC:def 2;
A65: CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A56,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now
assume
A66: AP<>{};
AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
.= P1A /\ P2B /\ CP;
then AP misses BP by A26,A27,A28;
hence contradiction by A52,A58,A59,A60,A64,A65,A66,CONNSP_1:11;
end;
hence thesis by A53,A65,XBOOLE_1:28;
end;
hence P1A is a_component &
P2B is a_component by A29,A34,A35;
end;
hence thesis;
end;
Lm10: for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
reconsider q=p as Point of Euclid 2 by EUCLID:22;
now per cases by A17;
suppose
A18: p`1 = s1 & p`2 <= t2 & p`2 >= t1;
now per cases by A18,XXREAL_0:1;
suppose
A19: p`1 = s1 & p`2 < t2 & p`2 > t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A20: Q is open and
A21: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A20,Lm9,PRE_TOPC:30;
then consider r be Real such that
A22: r>0 and
A23: Ball(q,r) c= Q by A21,TOPMETR:15;
reconsider r as Real;
A24: r/2>0 by A22,XREAL_1:215;
A25: r/20 by A1,XREAL_1:50;
A31: t2-t1>0 by A2,XREAL_1:50;
A32: (s2-s1)/2 >0 by A30,XREAL_1:215;
(t2-t1)/2>0 by A31,XREAL_1:215;
then 00 and
A46: Ball(q,r) c= Q by A44,TOPMETR:15;
reconsider r as Real;
A47: r/2>0 by A45,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A48: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A49: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A50: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A51: r2<=(s2-s1)/2 by A48,A49,XXREAL_0:2;
A52: r2<= (t2-t1)/2 by A48,A50,XXREAL_0:2;
A53: s2-s1>0 by A1,XREAL_1:50;
A54: t2-t1>0 by A2,XREAL_1:50;
A55: (s2-s1)/2 >0 by A53,XREAL_1:215;
(t2-t1)/2>0 by A54,XREAL_1:215;
then 0 s1 by A42,A56,A57,XREAL_1:29;
A60: pa`2> t1 by A42,A56,A58,XREAL_1:29;
(s2-s1)/2(r/2)^2+(r/2)^2 by A45,A47,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A65,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^20 and
A71: Ball(q,r) c= Q by A69,TOPMETR:15;
reconsider r as Real;
A72: r/2>0 by A70,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A73: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A74: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A75: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A76: r2<=(s2-s1)/2 by A73,A74,XXREAL_0:2;
A77: r2<= (t2-t1)/2 by A73,A75,XXREAL_0:2;
A78: s2-s1>0 by A1,XREAL_1:50;
A79: t2-t1>0 by A2,XREAL_1:50;
A80: (s2-s1)/2 >0 by A78,XREAL_1:215;
(t2-t1)/2>0 by A79,XREAL_1:215;
then 0 s1 by A67,A81,A82,XREAL_1:29;
A85: pa`2< t2 by A67,A81,A83,XREAL_1:44;
(s2-s1)/2t1 by A83,XREAL_1:12;
then
A87: pa in P1 by A4,A84,A85,A86;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A88: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A89: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A88,XREAL_1:7;
r2^2<= (r/2)^2 by A81,SQUARE_1:15,XXREAL_0:17;
then
A90: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A82,A83,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A70,A72,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A90,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= s1 & p`2 = t2;
now per cases by A92,XXREAL_0:1;
suppose
A93: p`2 = t2 & p`1 < s2 & p`1 > s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A94: Q is open and
A95: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A94,Lm9,PRE_TOPC:30;
then consider r be Real such that
A96: r>0 and
A97: Ball(q,r) c= Q by A95,TOPMETR:15;
reconsider r as Real;
A98: r/2>0 by A96,XREAL_1:215;
A99: r/20 by A1,XREAL_1:50;
A105: t2-t1>0 by A2,XREAL_1:50;
A106: (s2-s1)/2 >0 by A104,XREAL_1:215;
(t2-t1)/2>0 by A105,XREAL_1:215;
then 00 and
A119: Ball(q,r) c= Q by A117,TOPMETR:15;
reconsider r as Real;
A120: r/2>0 by A118,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A121: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A122: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A123: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A124: r2<=(s2-s1)/2 by A121,A122,XXREAL_0:2;
A125: r2<= (t2-t1)/2 by A121,A123,XXREAL_0:2;
A126: s2-s1>0 by A1,XREAL_1:50;
A127: t2-t1>0 by A2,XREAL_1:50;
A128: (s2-s1)/2 >0 by A126,XREAL_1:215;
(t2-t1)/2>0 by A127,XREAL_1:215;
then 0 s1 by A115,A129,A130,XREAL_1:29;
A133: pa`2< t2 by A115,A129,A131,XREAL_1:44;
(t2-t1)/2t1 by A131,XREAL_1:12;
(s2-s1)/2(r/2)^2+(r/2)^2 by A118,A120,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A138,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^20 and
A144: Ball(q,r) c= Q by A142,TOPMETR:15;
reconsider r as Real;
A145: r/2>0 by A143,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A146: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A147: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A148: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A149: r2<=(s2-s1)/2 by A146,A147,XXREAL_0:2;
A150: r2<= (t2-t1)/2 by A146,A148,XXREAL_0:2;
A151: s2-s1>0 by A1,XREAL_1:50;
A152: t2-t1>0 by A2,XREAL_1:50;
A153: (s2-s1)/2 >0 by A151,XREAL_1:215;
(t2-t1)/2>0 by A152,XREAL_1:215;
then 0s1 by A155,XREAL_1:12;
(t2-t1)/2t1 by A156,XREAL_1:12;
then
A160: pa in P1 by A4,A157,A158,A159;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A161: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A162: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A161,XREAL_1:7;
r2^2<= (r/2)^2 by A154,SQUARE_1:15,XXREAL_0:17;
then
A163: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A155,A156,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A143,A145,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A163,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= s1 & p`2 = t1;
now per cases by A165,XXREAL_0:1;
suppose
A166: p`2 = t1 & p`1 < s2 & p`1 > s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A167: Q is open and
A168: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A167,Lm9,PRE_TOPC:30;
then consider r be Real such that
A169: r>0 and
A170: Ball(q,r) c= Q by A168,TOPMETR:15;
reconsider r as Real;
A171: r/2>0 by A169,XREAL_1:215;
A172: r/20 by A1,XREAL_1:50;
A178: t2-t1>0 by A2,XREAL_1:50;
A179: (s2-s1)/2 >0 by A177,XREAL_1:215;
(t2-t1)/2>0 by A178,XREAL_1:215;
then 00 and
A193: Ball(q,r) c= Q by A191,TOPMETR:15;
reconsider r as Real;
A194: r/2>0 by A192,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A195: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A196: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A197: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A198: r2<=(s2-s1)/2 by A195,A196,XXREAL_0:2;
A199: r2<= (t2-t1)/2 by A195,A197,XXREAL_0:2;
A200: s2-s1>0 by A1,XREAL_1:50;
A201: t2-t1>0 by A2,XREAL_1:50;
A202: (s2-s1)/2 >0 by A200,XREAL_1:215;
(t2-t1)/2>0 by A201,XREAL_1:215;
then 0 s1 by A189,A203,A204,XREAL_1:29;
A207: pa`2> t1 by A189,A203,A205,XREAL_1:29;
(s2-s1)/2(r/2)^2+(r/2)^2 by A192,A194,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A212,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^20 and
A218: Ball(q,r) c= Q by A216,TOPMETR:15;
reconsider r as Real;
A219: r/2>0 by A217,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A220: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A221: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A222: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A223: r2<=(s2-s1)/2 by A220,A221,XXREAL_0:2;
A224: r2<= (t2-t1)/2 by A220,A222,XXREAL_0:2;
A225: s2-s1>0 by A1,XREAL_1:50;
A226: t2-t1>0 by A2,XREAL_1:50;
A227: (s2-s1)/2 >0 by A225,XREAL_1:215;
(t2-t1)/2>0 by A226,XREAL_1:215;
then 0 t1 by A214,A228,XREAL_1:29;
A232: pa`1< s2 by A214,A228,A229,XREAL_1:44;
(t2-t1)/2s1 by A229,XREAL_1:12;
then
A234: pa in P1 by A4,A231,A232,A233;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A235: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A236: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A235,XREAL_1:7;
r2^2<= (r/2)^2 by A228,SQUARE_1:15,XXREAL_0:17;
then
A237: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A229,A230,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A217,A219,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A237,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= t1;
now per cases by A239,XXREAL_0:1;
suppose
A240: p`1 = s2 & p`2 < t2 & p`2 > t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A241: Q is open and
A242: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A241,Lm9,PRE_TOPC:30;
then consider r being Real such that
A243: r>0 and
A244: Ball(q,r) c= Q by A242,TOPMETR:15;
reconsider r as Real;
A245: r/2>0 by A243,XREAL_1:215;
A246: r/20 by A1,XREAL_1:50;
A252: t2-t1>0 by A2,XREAL_1:50;
A253: (s2-s1)/2 >0 by A251,XREAL_1:215;
(t2-t1)/2>0 by A252,XREAL_1:215;
then 00 and
A266: Ball(q,r) c= Q by A264,TOPMETR:15;
reconsider r as Real;
A267: r/2>0 by A265,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A268: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A269: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A270: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A271: r2<=(s2-s1)/2 by A268,A269,XXREAL_0:2;
A272: r2<= (t2-t1)/2 by A268,A270,XXREAL_0:2;
A273: s2-s1>0 by A1,XREAL_1:50;
A274: t2-t1>0 by A2,XREAL_1:50;
A275: (s2-s1)/2 >0 by A273,XREAL_1:215;
(t2-t1)/2>0 by A274,XREAL_1:215;
then 0 t1 by A262,A276,A277,XREAL_1:29;
A280: pa`1< s2 by A262,A276,A278,XREAL_1:44;
(s2-s1)/2s1 by A278,XREAL_1:12;
(t2-t1)/2(r/2)^2+(r/2)^2 by A265,A267,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A285,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^20 and
A291: Ball(q,r) c= Q by A289,TOPMETR:15;
reconsider r as Real;
A292: r/2>0 by A290,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A293: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A294: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A295: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A296: r2<=(s2-s1)/2 by A293,A294,XXREAL_0:2;
A297: r2<= (t2-t1)/2 by A293,A295,XXREAL_0:2;
A298: s2-s1>0 by A1,XREAL_1:50;
A299: t2-t1>0 by A2,XREAL_1:50;
A300: (s2-s1)/2 >0 by A298,XREAL_1:215;
(t2-t1)/2>0 by A299,XREAL_1:215;
then 0s1 by A302,XREAL_1:12;
(t2-t1)/2t1 by A303,XREAL_1:12;
then
A307: pa in P1 by A4,A304,A305,A306;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A308: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A309: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A308,XREAL_1:7;
r2^2<= (r/2)^2 by A301,SQUARE_1:15,XXREAL_0:17;
then
A310: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A302,A303,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A290,A292,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A310,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds Cl P2 = P \/ P2
proof
let s1,t1,s2,t2;
let P,P2 be Subset of TOP-REAL 2;
assume that
A1: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
A5: P2 c= Cl P2 by PRE_TOPC:18;
reconsider P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
reconsider q=p as Point of Euclid 2 by EUCLID:22;
now per cases by A17;
suppose
A18: p`1 = s1 & p`2 <= t2 & p`2 >= t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A19: Q is open and
A20: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A19,Lm9,PRE_TOPC:30;
then consider r be Real such that
A21: r>0 and
A22: Ball(q,r) c= Q by A20,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1-r/2,p`2]|;
A23: pa`1=p`1-r/2 by EUCLID:52;
A24: pa`2=p`2 by EUCLID:52;
A25: r/2>0 by A21,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A18,A21,A23,
XREAL_1:44,215;
then
A26: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A27: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A28: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A27,XREAL_1:7;
p`1 - pa`1 < r by A21,A23,XREAL_1:216;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A23,A24,A25,SQUARE_1:16
;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2 {} by A22,A26,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
suppose
A30: p`1 <= s2 & p`1 >= s1 & p`2 = t2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A31: Q is open and
A32: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A31,Lm9,PRE_TOPC:30;
then consider r being Real such that
A33: r>0 and
A34: Ball(q,r) c= Q by A32,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1,p`2+r/2]|;
A35: pa`1=p`1 by EUCLID:52;
A36: pa`2=p`2+r/2 by EUCLID:52;
A37: r/2>0 by A33,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A30,A33,A36,
XREAL_1:29,215;
then
A38: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A39: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A40: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A39,XREAL_1:7;
A41: pa`2 - p`2 < r by A33,A36,XREAL_1:216;
(pa`2-p`2)^2=(p`2-pa`2)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A35,A36,A37,A41,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2 {} by A34,A38,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
suppose
A43: p`1 <= s2 & p`1 >= s1 & p`2 = t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A44: Q is open and
A45: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A44,Lm9,PRE_TOPC:30;
then consider r being Real such that
A46: r>0 and
A47: Ball(q,r) c= Q by A45,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1,p`2-r/2]|;
A48: pa`1=p`1 by EUCLID:52;
A49: pa`2=p`2-r/2 by EUCLID:52;
A50: r/2>0 by A46,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A43,A46,A49,XREAL_1:44,215;
then
A51: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A52: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A53: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A52,XREAL_1:7;
p`2 - pa`2 < r by A46,A49,XREAL_1:216;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A48,A49,A50,SQUARE_1:16
;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A56: Q is open and
A57: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A56,Lm9,PRE_TOPC:30;
then consider r being Real such that
A58: r>0 and
A59: Ball(q,r) c= Q by A57,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1+r/2,p`2]|;
A60: pa`1=p`1+r/2 by EUCLID:52;
A61: pa`2=p`2 by EUCLID:52;
A62: r/2>0 by A58,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A55,A58,A60,XREAL_1:29,215;
then
A63: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A64: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A65: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A64,XREAL_1:7;
A66: pa`1 - p`1 < r by A58,A60,XREAL_1:216;
(pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A60,A61,A62,A66,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
= s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
then ex p being Point of TOP-REAL 2 st p=x & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
hence contradiction by A4;
end;
then x in P` by A1,A3,SUBSET_1:29;
hence thesis by PRE_TOPC:def 5;
end;
theorem
for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
= s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 c= [#]((TOP-REAL 2)|P`)
proof
let s1,s2,t1,t2,P,P2;
assume that
A1: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
let x be object;
assume
A5: x in P2;
then
A6: ex pa being Point of TOP-REAL 2 st pa=x &
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A4;
now
assume x in { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
then ex p being Point of TOP-REAL 2 st p=x & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
hence contradiction by A1,A2,A6;
end;
then x in P` by A3,A5,SUBSET_1:29;
hence thesis by PRE_TOPC:def 5;
end;
theorem
for s1,s2,t1,t2,P,P2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 is Subset of (TOP-REAL 2)|P`
proof
let s1,s2,t1,t2,P,P2;
assume that
A1: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
P2 c= [#]((TOP-REAL 2)|P`) by A1,A2,A3,A4,Th34;
hence thesis;
end;
begin
::
:: The Jordan's property
::
definition
let S be Subset of TOP-REAL 2;
attr S is Jordan means
S`<> {} & ex A1,A2 being Subset of TOP-REAL 2 st
S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
for C1,C2 being Subset of (TOP-REAL 2)|S` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component;
end;
theorem
for S being Subset of TOP-REAL 2 st S is Jordan holds S`<> {} &
ex A1,A2 being Subset of TOP-REAL 2 st
ex C1,C2 being Subset of (TOP-REAL 2)|S` st S` = A1 \/ A2 & A1 misses A2 &
(Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 &
C1 is a_component & C2 is a_component &
for C3 being Subset of (TOP-REAL 2)|S` st C3 is a_component holds
C3 = C1 or C3 = C2
proof
let S be Subset of TOP-REAL 2;
assume
A1: S is Jordan;
then reconsider S9 = S` as non empty Subset of TOP-REAL 2;
consider A1,A2 being Subset of TOP-REAL 2 such that
A2: S`=A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1)\A1=(Cl A2)\A2 and
A5: for C1,C2 being Subset of (TOP-REAL 2)|S`
st C1=A1 & C2=A2 holds C1 is a_component & C2 is a_component by A1;
A6: A1 c= S` by A2,XBOOLE_1:7;
A7: A2 c= S` by A2,XBOOLE_1:7;
A8: [#]((TOP-REAL 2)|S`)=S` by PRE_TOPC:def 5;
A1 c= [#]((TOP-REAL 2)|S`) by A6,PRE_TOPC:def 5;
then reconsider G0A=A1,G0B=A2 as Subset of (TOP-REAL 2)|S9 by A7,
PRE_TOPC:def 5;
A9: G0A=A1;
G0B=A2;
then
A10: G0A is a_component by A5;
A11: G0B is a_component by A5,A9;
now
let C3 be Subset of (TOP-REAL 2)|S9;
assume
A12: C3 is a_component;
then
A13: C3 <>{}((TOP-REAL 2)|S9) by CONNSP_1:32;
C3 /\(G0A \/ G0B)=C3 by A2,A8,XBOOLE_1:28;
then
A14: (C3 /\ G0A) \/ (C3 /\ G0B) <>{} by A13,XBOOLE_1:23;
now per cases by A14;
suppose C3 /\ G0A<>{};
then
A15: C3 meets G0A;
A16: C3 is connected by A12;
A17: G0A is connected by A10;
then
A18: C3 \/ G0A is connected by A15,A16,CONNSP_1:1,17;
G0A c= C3 \/ G0A by XBOOLE_1:7;
then G0A=C3 \/ G0A by A10,A18;
then C3 c= G0A by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A12,A17;
end;
suppose C3 /\ A2<>{};
then
A19: C3 meets G0B;
A20: C3 is connected by A12;
A21: G0B is connected by A11;
then
A22: C3 \/ G0B is connected by A19,A20,CONNSP_1:1,17;
G0B c= C3 \/ G0B by XBOOLE_1:7;
then G0B=C3 \/ G0B by A11,A22;
then C3 c= G0B by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A12,A21;
end;
end;
hence C3=G0A or C3=G0B;
end;
hence thesis by A2,A3,A4,A10,A11;
end;
theorem
for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} holds P is Jordan
proof
let s1,s2,t1,t2;
let P be Subset of TOP-REAL 2;
assume that
A1: s1= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
reconsider P1= {pa where pa is Point of TOP-REAL 2:
s1{} by A1,A2,A3,A4,A5,Th30;
A8: P1 misses P2 by A1,A2,A3,Th30;
A9: P=(Cl P1)\P1 by A1,A2,A3,A5,Th31;
A10: P=(Cl P2)\P2 by A1,A2,A3,A4,Th31;
for P1A,P2B be Subset of (TOP-REAL 2)|P` holds P1A=P1 & P2B=P2 implies
P1A is a_component & P2B is a_component by A1,A2,A3,Th30;
hence thesis by A6,A7,A8,A9,A10;
end;
theorem
for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds Cl P2 = P \/ P2 by Lm11;
theorem
for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1 p by A5,TARSKI:def 2;
A8: w2 <> p by A6,TARSKI:def 2;
A9: w1 <> q by A5,TARSKI:def 2;
A10: w2 <> q by A6,TARSKI:def 2;
A11: not p in LSeg(w1,w2) by A3,A4,A7,A8,SPPOL_1:7,TOPREAL1:6;
not q in LSeg(w1,w2) by A3,A4,A9,A10,SPPOL_1:7,TOPREAL1:6;
then LSeg(w1,w2) misses {p,q} by A11,ZFMISC_1:51;
hence thesis by A3,A4,TOPREAL1:6,XBOOLE_1:86;
end;
:: Moved from JORDAN1A, AK, 22.02.2006
Lm12: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x <= x0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x,y0 ]| where x is Real : x <= x0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 <= x0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 <= x0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x1,(1-l)*y0 ]| + l*|[ x2,y0 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x1,(1-l)*y0 ]| + |[ l*x2,l*y0 ]| by EUCLID:58
.= |[ (1-l)*x1+l*x2,(1-l)*y0+l*y0 ]| by EUCLID:56
.= |[ (1-l)*x1+l*x2,1 * y0 ]|;
(1-l)*x1+l*x2 <= x0 by A5,A7,A10,A11,XREAL_1:174;
hence thesis by A1,A12;
end;
Lm13: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y <= y0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x0,y ]| where y is Real : y <= y0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider y1 being Real such that
A4: w1 = |[ x0,y1 ]| and
A5: y1 <= y0 by A1,A2;
consider y2 being Real such that
A6: w2 = |[ x0,y2 ]| and
A7: y2 <= y0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x0,(1-l)*y1 ]| + l*|[ x0,y2 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x0,(1-l)*y1 ]| + |[ l*x0,l*y2 ]| by EUCLID:58
.= |[ (1-l)*x0+l*x0,(1-l)*y1+l*y2 ]| by EUCLID:56
.= |[ 1 * x0,(1-l)*y1+l*y2 ]|;
(1-l)*y1+l*y2 <= y0 by A5,A7,A10,A11,XREAL_1:174;
hence thesis by A1,A12;
end;
Lm14: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x >= x0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x,y0 ]| where x is Real : x >= x0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 >= x0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 >= x0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
by A8,RLTOPSP1:def 2;
then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x2,(1-l)*y0 ]| + l*|[ x1,y0 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x2,(1-l)*y0 ]| + |[ l*x1,l*y0 ]| by EUCLID:58
.= |[ (1-l)*x2+l*x1,(1-l)*y0+l*y0 ]| by EUCLID:56
.= |[ (1-l)*x2+l*x1,1 * y0 ]|;
(1-l)*x2+l*x1 >= x0 by A5,A7,A10,A11,XREAL_1:173;
hence thesis by A1,A12;
end;
Lm15: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y >= y0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x0,y ]| where y is Real : y >= y0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x0,x1 ]| and
A5: x1 >= y0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x0,x2 ]| and
A7: x2 >= y0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
by A8,RLTOPSP1:def 2;
then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x0,(1-l)*x2 ]| + l*|[ x0,x1 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x0,(1-l)*x2 ]| + |[ l*x0,l*x1 ]| by EUCLID:58
.= |[ (1-l)*x0+l*x0,(1-l)*x2+l*x1 ]| by EUCLID:56
.= |[ 1 * x0,(1-l)*x2+l*x1]|;
(1-l)*x2+l*x1 >= y0 by A5,A7,A10,A11,XREAL_1:173;
hence thesis by A1,A12;
end;
registration
let p be Point of TOP-REAL 2;
cluster north_halfline p -> convex;
coherence
proof
north_halfline p =
{ |[ p`1,r ]| where r is Real: r >= p`2 } by TOPREAL1:31;
hence thesis by Lm15;
end;
cluster east_halfline p -> convex;
coherence
proof
east_halfline p =
{ |[ r,p`2 ]| where r is Real: r >= p`1 } by TOPREAL1:33;
hence thesis by Lm14;
end;
cluster south_halfline p -> convex;
coherence
proof
south_halfline p =
{ |[ p`1,r ]| where r is Real: r <= p`2 } by TOPREAL1:35;
hence thesis by Lm13;
end;
cluster west_halfline p -> convex;
coherence
proof
west_halfline p =
{ |[ r,p`2 ]| where r is Real: r <= p`1 } by TOPREAL1:37;
hence thesis by Lm12;
end;
end;
~~