Copyright (c) 1992 Association of Mizar Users
environ
vocabulary PRE_TOPC, FUNCT_1, RELAT_1, SUBSET_1, RELAT_2, ORDINAL2, BOOLE,
RCOMP_1, BORSUK_1, FUNCOP_1, CONNSP_1, EUCLID, TOPREAL1, TOPS_2, ARYTM_1,
MCART_1, ARYTM_3, SQUARE_1, PCOMPS_1, METRIC_1, JORDAN1, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, REAL_1, RELAT_1,
NAT_1, FUNCT_1, FUNCT_2, BINOP_1, PRE_TOPC, TOPS_2, CONNSP_1, SQUARE_1,
RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1, TOPREAL1, EUCLID;
constructors REAL_1, TOPS_2, CONNSP_1, SQUARE_1, RCOMP_1, TOPMETR, TOPREAL1,
MEMBERED, NAT_1;
clusters PRE_TOPC, BORSUK_1, STRUCT_0, EUCLID, TOPREAL1, XREAL_0, RELSET_1,
MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, CONNSP_1, XBOOLE_0;
theorems TARSKI, AXIOMS, REAL_1, FUNCOP_1, FUNCT_1, FUNCT_2, SUBSET_1,
RCOMP_1, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, SEQ_2, CONNSP_1,
SQUARE_1, REAL_2, TOPMETR, TOPREAL1, EUCLID, TOPREAL3, TREAL_1, RELAT_1,
XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_0, XCMPLX_1;
begin
::
:: Selected theorems on connected space
::
reserve GX,GY for non empty TopSpace,
x,y for Point of GX,
r,s for Real;
theorem Th1:
for GX being TopStruct,
A being Subset of GX holds the carrier of (GX|A) = A
proof
let GX be TopStruct, A be Subset of GX;
A=[#](GX|A) by PRE_TOPC:def 10;
hence thesis by PRE_TOPC:12;
end;
theorem Th2:
for GX being non empty TopSpace st
(for x,y being Point of GX ex GY st (GY is connected &
ex f being map of GY,GX st
f is continuous & x in rng(f)& y in rng(f))) holds
GX is connected
proof let GX;
assume A1:(for x,y being Point of GX ex GY st (GY is connected &
ex f being map of GY,GX st f is continuous
& x in rng f & y in rng f));
for A,B being Subset of GX
st [#](GX) = A \/ B & A <> {}(GX) & B <> {}(GX) & A is open &
B is open holds A meets B
proof let A,B be Subset of GX;assume that
A2:[#](GX) = A \/ B and A3: A <> {}(GX) and A4: B <> {}(GX)
and A5: A is open and A6: B is open;
consider u being Element of A;
u in [#](GX) by A2,A3,XBOOLE_0:def 2;
then reconsider x=u as Point of GX;
consider v being Element of B;
v in [#](GX) by A2,A4,XBOOLE_0:def 2;
then reconsider y=v as Point of GX;
consider GY such that A7: GY is connected
and A8: ex f being map of GY,GX
st f is continuous & x in rng f & y in rng f by A1;
consider f being map of GY,GX such that
A9: f is continuous and A10: x in rng f and A11: y in rng f by A8;
A12:f"A is open by A5,A9,TOPS_2:55;
A13:f"B is open by A6,A9,TOPS_2:55;
f"([#] GX)=[#] GY by TOPS_2:52;
then A14:f"A \/ f"B = [#] GY by A2,RELAT_1:175;
rng f /\ A <> {} by A3,A10,XBOOLE_0:def 3;
then rng f meets A by XBOOLE_0:def 7;
then A15:f"A <> {}(GY) by RELAT_1:173;
rng f /\ B <> {} by A4,A11,XBOOLE_0:def 3;
then rng f meets B by XBOOLE_0:def 7;
then f"B <> {}(GY) by RELAT_1:173;
then f"A meets f"B by A7,A12,A13,A14,A15,CONNSP_1:12;
then f"A /\ f"B <> {} by XBOOLE_0:def 7;
then f"(A /\ B) <> {} by FUNCT_1:137;
then rng f meets (A /\ B) by RELAT_1:173;
then consider u1 being set such that
A16: u1 in rng f & u1 in A /\ B by XBOOLE_0:3;
thus thesis by A16,XBOOLE_0:4;
end;
hence thesis by CONNSP_1:12;
end;
Lm1: 0 in [.0,1.] & 1 in [.0,1.]
proof
0 in {r:0<=r & r<=1} & 1 in {s:0<=s & s<=1};
hence thesis by RCOMP_1:def 1;
end;
canceled;
theorem Th4: ::Arcwise connectedness derives connectedness
for GX being non empty TopSpace st
(for x,y being Point of GX
ex h being map 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 map 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 map of GY,GX st f is continuous
& x in rng(f)& y in rng(f))
proof let x,y;
now
consider h being map of I[01],GX such that
A2: h is continuous and A3: x=h.0 & y=h.1 by A1;
[#] I[01] = the carrier of I[01] by PRE_TOPC:12;
then 0 in dom h & 1 in dom h by Lm1,BORSUK_1:83,TOPS_2:51;
then x in rng h & y in rng h by A3,FUNCT_1:def 5;
hence thesis by A2,TREAL_1:22;
end;
hence thesis;
end;
hence thesis by Th2;
end;
theorem Th5: ::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 map 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 map 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 map of I[01],GX|A st h is continuous
& xa=h.0 & ya=h.1
proof
let xa,ya be Point of GX; assume
A3: xa in A & ya in A & xa = ya;
then xa in the carrier of (GX|A) by Th1;
then reconsider xa' = xa as Element of GX|A;
reconsider h = I[01] --> xa' as map of I[01], GX|A;
take h;
h = (the carrier of I[01]) --> xa' by BORSUK_1:def 3;
hence thesis by A3,Lm1,BORSUK_1:36,83,FUNCOP_1:13;
end;
for xb,yb being Point of GX|A
ex ha being map of I[01],GX|A st ha is continuous
& xb=ha.0 & yb=ha.1
proof
let xb,yb be Point of GX|A;
xb in the carrier of (GX|A) & yb in the carrier of (GX|A);
then xb in [#](GX|A) & yb in [#](GX|A) by PRE_TOPC:12;
then A4: xb in A & yb in A by PRE_TOPC:def 10;
per cases;
suppose xb<>yb;
hence thesis by A1,A4;
suppose xb = yb;
hence thesis by A2,A4;
end;
then GX|A is connected by Th4;
hence thesis by CONNSP_1:def 3;
suppose A is empty;
then reconsider D = A as empty Subset of GX;
let A1, B1 be Subset of GX|A such that
A5: [#](GX|A) = A1 \/ B1 and A1,B1 are_separated;
[#](GX|D) = D by PRE_TOPC:def 10;
hence A1 = {}(GX|A) or B1 = {}(GX|A) by A5,XBOOLE_1:15;
end;
theorem Th6:
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
proof let A0 be Subset of GX,
A1 be Subset of GX;
assume that A1: A0 is connected & A1 is connected and
A2: A0 meets A1;
not A0,A1 are_separated by A2,CONNSP_1:2;
hence thesis by A1,CONNSP_1:18;
end;
theorem Th7:
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 & A1 is connected & A2 is connected and
A2: A0 meets A1 & A1 meets A2;
A3: A0 /\ A1 <> {} & A1 /\ A2 <> {} by A2,XBOOLE_0:def 7;
A4: A0 \/ A1 is connected by A1,A2,Th6;
(A0 \/ A1)/\ A2= A0 /\ A2 \/ A1 /\ A2 by XBOOLE_1:23;
then (A0 \/ A1) /\ A2 <> {} by A3,XBOOLE_1:15;
then (A0 \/ A1) meets A2 by XBOOLE_0:def 7;
hence thesis by A1,A4,Th6;
end;
theorem Th8:
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 &
A1 is connected & A2 is connected & A3 is connected and
A2: A0 meets A1 & A1 meets A2 & A2 meets A3;
A3: A0 /\ A1 <> {} & A1 /\ A2 <> {} & A2 /\ A3 <> {} by A2,XBOOLE_0:def 7;
A4: A0 \/ A1 \/ A2 is connected by A1,A2,Th7;
(A0 \/ A1 \/ A2)/\ A3= (A0 \/ A1) /\ A3 \/ A2 /\ A3 by XBOOLE_1:23;
then (A0 \/ A1 \/ A2) /\ A3 <> {} by A3,XBOOLE_1:15;
then (A0 \/ A1 \/ A2) meets A3 by XBOOLE_0:def 7;
hence thesis by A1,A4,Th6;
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 n be Nat, P be Subset of TOP-REAL n;
attr P is convex means
for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P holds
LSeg(w1,w2) c= P;
end;
theorem Th9:
for n being Nat, P being Subset of TOP-REAL n st P is convex holds
P is connected
proof let n be Nat, 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 map 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 A2:w1 in P & w2 in P & w1<>w2;
then A3: LSeg(w1,w2) c= P by A1;
LSeg(w1,w2) is_an_arc_of w1,w2 by A2,TOPREAL1:15;
then consider f being map of I[01], (TOP-REAL n)|LSeg(w1,w2) such that
A4: f is_homeomorphism & f.0 = w1 & f.1 = w2 by TOPREAL1:def 2;
A5:f is continuous by A4,TOPS_2:def 5;
A6: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A4,TOPS_2:def 5;
then A7: rng f c= P by A3,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
by A6,PRE_TOPC:def 10;
then [#]((TOP-REAL n)|LSeg(w1,w2))
c=the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then the carrier of ((TOP-REAL n)|LSeg(w1,w2))
c= the carrier of ((TOP-REAL n)|P) by PRE_TOPC:12;
then A8:(TOP-REAL n)|LSeg(w1,w2)
is SubSpace of (TOP-REAL n)|P by TOPMETR:4;
dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
then reconsider g=f as Function of [.0,1.],P by A7,FUNCT_2:4;
the carrier of (TOP-REAL n)|P =
[#]((TOP-REAL n)|P) by PRE_TOPC:12 .= P by PRE_TOPC:def 10;
then reconsider gt=g as map of I[01],(TOP-REAL n)|P by BORSUK_1:83;
gt is continuous by A5,A8,TOPMETR:7;
hence thesis by A4;
end;
hence thesis by Th5;
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,lambda,sa,sd,ta,td for Real;
theorem Th10:
s1<s3 & s1<s4 & 0 <= l & l <= 1 implies s1<(1-l)*s3+l*s4
proof
assume A1:s1<s3 & s1<s4 & 0 <= l & l <= 1;
now per cases;
suppose l=0;
hence thesis by A1;
suppose l=1;
hence thesis by A1;
suppose A2: not(l=0 or l=1);
then A3: l>0 & l<1 by A1,REAL_1:def 5;
A4:l*s1<l*s4 by A1,A2,REAL_1:70; 1-l>0 by A3,SQUARE_1:11;
then A5: (1-l)*s1<(1-l)*s3 by A1,REAL_1:70;
(1-l)*s1+l*s1=(1-l+l)*s1 by XCMPLX_1:8
.=1*s1 by XCMPLX_1:27
.=s1;
hence thesis by A4,A5,REAL_1:67;
end;
hence thesis;
end;
theorem Th11:
s3<s1 & s4<s1 & 0 <= l & l <= 1 implies (1-l)*s3+l*s4<s1
proof
assume A1:s1>s3 & s1>s4 & 0 <= l & l <= 1;
now per cases;
suppose l=0;
hence thesis by A1;
suppose l=1;
hence thesis by A1;
suppose A2: not(l=0 or l=1);
then A3: l>0 & l<1 by A1,REAL_1:def 5;
A4:l*s1>l*s4 by A1,A2,REAL_1:70; 1-l>0 by A3,SQUARE_1:11;
then A5: (1-l)*s1>(1-l)*s3 by A1,REAL_1:70;
(1-l)*s1+l*s1=(1-l+l)*s1 by XCMPLX_1:8
.=1*s1 by XCMPLX_1:27
.=s1;
hence thesis by A4,A5,REAL_1:67;
end;
hence thesis;
end;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;
Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25;
Lm3: for s1 holds { |[ sb,tb ]|:sb<s1} is Subset of REAL 2
proof let s1;
{ |[ sb,tb ]|:sb<s1} c= REAL 2
proof let y be set;assume y in { |[ sb,tb ]|:sb<s1};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & s7<s1;
hence thesis by Lm2;
end;
hence thesis;
end;
Lm4: for t1 holds { |[ sb,tb ]| :tb<t1} is Subset of REAL 2
proof let t1;
{ |[ sd,td ]|:td<t1} c= REAL 2
proof let y be set;assume y in { |[ sd,td ]|:td<t1};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & t7<t1;
hence thesis by Lm2;
end;
hence thesis;
end;
Lm5: for s2 holds { |[ sb,tb ]| :s2<sb} is Subset of REAL 2
proof let s2;
{ |[ sb,tb ]|:s2<sb} c= REAL 2
proof let y be set;assume y in { |[ sb,tb ]|:s2<sb};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & s2<s7;
hence thesis by Lm2;
end;
hence thesis;
end;
Lm6: for t2 holds { |[ sb,tb ]|:t2<tb} is Subset of REAL 2
proof let t2;
{ |[ sb,tb ]|:t2<tb} c= REAL 2
proof let y be set;assume y in { |[ sb,tb ]|:t2<tb};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & t2<t7;
hence thesis by Lm2;
end;
hence thesis;
end;
Lm7: for s1,s2,t1,t2 holds
{ |[ s,t ]| where s is Real,t is Real:
s1<s & s<s2 & t1<t & t<t2} is Subset of REAL 2
proof let s1,s2,t1,t2;
{ |[ sb,tb ]| where sb is Real, tb is Real:
s1<sb & sb<s2 & t1<tb & tb<t2} c= REAL 2
proof let y be set;assume
y in { |[ sb,tb ]| where sb is Real,tb is Real:
s1<sb & sb<s2 & t1<tb & tb<t2};
then ex s7,t7 being Real st |[ s7,t7 ]|=y &
s1<s7 & s7<s2 & t1<t7 & t7<t2;
hence thesis by Lm2;
end;
hence thesis;
end;
Lm8: for s1,s2,t1,t2 holds
{ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} is Subset of REAL 2
proof let s1,s2,t1,t2;
{ |[ sb,tb ]|
where sb is Real,tb is Real:
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} c= REAL 2
proof let y be set;assume y in { |[ sb,tb ]| where sb is Real,tb is Real:
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
then ex s7,t7 being Real st |[ s7,t7 ]|=y &
not (s1<=s7 & s7<=s2 & t1<=t7 & t7<=t2);
hence thesis by Lm2;
end;
hence thesis;
end;
theorem Th12:
{|[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} =
{|[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2} /\ {|[s5,t5]|:t1<t5} /\
{|[s6,t6]|:t6<t2}
proof
now let x be set;assume
x in { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2};
then ex s,t st |[s,t]|=x & (s1<s & s<s2 & t1<t & t<t2);
then x in { |[ s3,t3 ]|:s1<s3} & x in { |[ s4,t4 ]|:s4<s2}
& x in { |[ s5,t5 ]|:t1<t5} & x in { |[ s6,t6 ]|:t6<t2};
then x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4 ]|:s4<s2}
& x in { |[ s5,t5 ]|:t1<t5} & x in { |[ s6,t6 ]|:t6<t2} by XBOOLE_0:def 3
;
then x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
& x in { |[ s6,t6 ]|:t6<t2} by XBOOLE_0:def 3;
hence x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2} by XBOOLE_0:def 3;
end; then A1: { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} c=
{ |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2} by TARSKI:def 3;
now let x be set;assume
x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2};
then x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
& x in { |[ s6,t6 ]|:t6<t2} by XBOOLE_0:def 3;
then x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4]|:s4<s2}
& x in { |[ s5,t5 ]|:t1<t5} & x in { |[ s6,t6 ]|:t6<t2} by XBOOLE_0:def 3
;
then A2: x in { |[ s3,t3 ]|:s1<s3} & x in { |[ s4,t4 ]|:s4<s2}
& x in { |[ s5,t5 ]|:t1<t5} & x in { |[ s6,t6 ]|:t6<t2} by XBOOLE_0:def 3
;
then A3:(ex sa,ta st |[sa,ta]|=x & s1<sa)
& (ex sb,tb st |[sb,tb]|=x & sb<s2)
& (ex sc,tc st |[sc,tc]|=x & t1<tc)
& (ex sd,td st |[sd,td]|=x & td<t2);
consider sa,ta such that A4:|[sa,ta]|=x & s1<sa by A2;
reconsider p=x as Point of TOP-REAL 2 by A3;
p`1=sa & p`2=ta by A4,EUCLID:56;
then |[sa,ta]|=x & s1<sa & sa<s2 & t1<ta & ta<t2
by A3,A4,EUCLID:56;
hence x in { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
end;
then { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2}c={ |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
by TARSKI:def 3;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th13:
{|[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} =
{|[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1} \/ {|[s5,t5]|:s2<s5} \/
{|[s6,t6]|:t2<t6}
proof
now let x be set;assume
x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
then ex s,t st |[s,t]|=x & not (s1<=s & s<=s2 & t1<=t & t<=t2);
then x in { |[ s3,t3 ]|:s3<s1}or x in { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6};
then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def
2;
then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 2;
hence x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by XBOOLE_0:def 2;
end; then A1: { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} c=
{ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by TARSKI:def 3;
now let x be set;assume
x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6};
then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 2;
then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def
2;
then x in { |[ s3,t3 ]|:s3<s1} or x in { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def
2;
then (ex sa,ta st |[sa,ta]|=x & sa<s1)
or (ex sc,tc st |[sc,tc]|=x & tc<t1)
or (ex sb,tb st |[sb,tb]|=x & s2<sb)
or (ex sd,td st |[sd,td]|=x & t2<td);
hence x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
end;
then { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6}c={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
by TARSKI:def 3;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th14:
for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
holds P is convex
proof let s1,t1,s2,t2,P;
assume A1:P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
let w1,w2 such that A2: w1 in P & w2 in P;
let x be set such that A3: x in LSeg(w1,w2);
consider s3,t3 such that
A4:|[ s3,t3 ]|=w1 & (s1<s3 & s3<s2 & t1<t3 & t3<t2) by A1,A2;
A5: w1`1=s3 & w1`2=t3 by A4,EUCLID:56;
consider s4,t4 such that
A6:|[ s4,t4 ]|=w2 & (s1<s4 & s4<s2 & t1<t4 & t4<t2) by A1,A2;
A7: w2`1=s4 & w2`2=t4 by A6,EUCLID:56;
x in {(1-lambda)*w1 + lambda*w2: 0 <= lambda & lambda <=
1} by A3,TOPREAL1:def 4;
then consider l such that A8: x = (1-l)*w1 + l*w2 & 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:59;
(1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| & l*w2=|[ l*w2`1 ,l*w2`2 ]|
by EUCLID:61;
then ((1-l)*w1)`1= (1-l)*w1`1 & ((1-l)*w1)`2= (1-l)*w1`2
& (l*w2)`1=l*w2`1 & (l*w2)`2=l*w2`2 by EUCLID:56;
then w`1=(1-l)* w1`1+ l* w2`1 & w`2=(1-l)* w1`2+ l* w2`2 by A9,EUCLID:56;
then s1< w`1 & w`1<s2 & t1< w`2 & w`2<t2 &
w = |[w`1, w`2]| by A4,A5,A6,A7,A8,Th10,Th11,EUCLID:57;
hence thesis by A1,A8;
end;
theorem Th15:
for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
holds P is connected
proof let s1,t1,s2,t2,P;
assume P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
then P is convex by Th14;
hence thesis by Th9;
end;
theorem Th16:
for s1,P st P = { |[ s,t ]|:s1<s } holds P is convex
proof let s1,P;
assume A1:P = { |[ s,t ]|:s1<s };
let w1,w2 such that A2: w1 in P & w2 in P;
let x be set such that A3: x in LSeg(w1,w2);
consider s3,t3 such that
A4:|[ s3,t3 ]|=w1 & s1<s3 by A1,A2;
A5: w1`1=s3 & w1`2=t3 by A4,EUCLID:56;
consider s4,t4 such that
A6:|[ s4,t4 ]|=w2 & s1<s4 by A1,A2;
A7: w2`1=s4 & w2`2=t4 by A6,EUCLID:56;
x in {(1-lambda)*w1 + lambda*w2: 0 <= lambda & lambda <=
1} by A3,TOPREAL1:def 4;
then consider l such that A8: x = (1-l)*w1 + l*w2& 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:59;
(1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| & l*w2=|[ l*w2`1 ,l*w2`2 ]|
by EUCLID:61;
then ((1-l)*w1)`1= (1-l)*w1`1 & ((1-l)*w1)`2= (1-l)*w1`2
& (l*w2)`1=l*w2`1 & (l*w2)`2=l*w2`2 by EUCLID:56;
then w`1=(1-l)* w1`1+ l* w2`1 & w`2=(1-l)* w1`2+ l* w2`2 by A9,EUCLID:56;
then s1< w`1 &
w = |[w`1, w`2]| by A4,A5,A6,A7,A8,Th10,EUCLID:57;
hence thesis by A1,A8;
end;
theorem Th17:
for s1,P st P = { |[ s,t ]|:s1<s } holds P is connected
proof let s1,P;
assume A1:P = { |[ s,t ]|:s1<s };
set s3 =s1+1; s1<s3 by REAL_2:174;
then |[ s3,0 ]| in { |[ s,t ]|:s1<s };
then P is convex non empty by A1,Th16;
hence thesis by Th9;
end;
theorem Th18:
for s2,P st P = {|[ s,t ]|:s<s2 } holds P is convex
proof let s2,P;
assume A1:P = { |[ s,t ]|:s<s2 };
let w1,w2 such that A2: w1 in P & w2 in P;
let x be set such that A3: x in LSeg(w1,w2);
consider s3,t3 such that
A4:|[ s3,t3 ]|=w1 & s3<s2 by A1,A2;
A5: w1`1=s3 & w1`2=t3 by A4,EUCLID:56;
consider s4,t4 such that
A6:|[ s4,t4 ]|=w2 & s4<s2 by A1,A2;
A7: w2`1=s4 & w2`2=t4 by A6,EUCLID:56;
x in {(1-lambda)*w1 + lambda*w2: 0 <= lambda & lambda <=
1} by A3,TOPREAL1:def 4;
then consider l such that A8: x = (1-l)*w1 + l*w2& 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:59;
(1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| & l*w2=|[ l*w2`1 ,l*w2`2 ]|
by EUCLID:61;
then ((1-l)*w1)`1= (1-l)*w1`1 & ((1-l)*w1)`2= (1-l)*w1`2
& (l*w2)`1=l*w2`1 & (l*w2)`2=l*w2`2 by EUCLID:56;
then w`1=(1-l)* w1`1+ l* w2`1 & w`2=(1-l)* w1`2+ l* w2`2 by A9,EUCLID:56;
then s2> w`1 &
w = |[w`1, w`2]| by A4,A5,A6,A7,A8,Th11,EUCLID:57;
hence thesis by A1,A8;
end;
theorem Th19:
for s2,P st P = {|[ s,t ]|:s<s2 } holds P is connected
proof let s2,P;
assume A1:P = { |[ s,t ]|:s<s2 };
set s3 =s2-1; s3<s2 by REAL_2:174;
then |[ s3,0 ]| in { |[ s,t ]|:s<s2 };
then P is convex non empty by A1,Th18;
hence thesis by Th9;
end;
theorem Th20:
for t1,P st P = {|[ s,t ]|:t1<t } holds P is convex
proof let t1,P;
assume A1:P = { |[ s,t ]|:t1<t };
let w1,w2 such that A2: w1 in P & w2 in P;
let x be set such that A3: x in LSeg(w1,w2);
consider s3,t3 such that
A4:|[ s3,t3 ]|=w1 & t1<t3 by A1,A2;
A5: w1`1=s3 & w1`2=t3 by A4,EUCLID:56;
consider s4,t4 such that
A6:|[ s4,t4 ]|=w2 & t1<t4 by A1,A2;
A7: w2`1=s4 & w2`2=t4 by A6,EUCLID:56;
x in {(1-lambda)*w1 + lambda*w2: 0 <= lambda & lambda <=
1} by A3,TOPREAL1:def 4;
then consider l such that A8: x = (1-l)*w1 + l*w2& 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:59;
(1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| & l*w2=|[ l*w2`1 ,l*w2`2 ]|
by EUCLID:61;
then ((1-l)*w1)`1= (1-l)*w1`1 & ((1-l)*w1)`2= (1-l)*w1`2
& (l*w2)`1=l*w2`1 & (l*w2)`2=l*w2`2 by EUCLID:56;
then w`1=(1-l)* w1`1+ l* w2`1 & w`2=(1-l)* w1`2+ l* w2`2 by A9,EUCLID:56;
then t1< w`2 & w = |[w`1, w`2]| by A4,A5,A6,A7,A8,Th10,EUCLID:57;
hence thesis by A1,A8;
end;
theorem Th21:
for t1,P st P = {|[ s,t ]|:t1<t } holds P is connected
proof let t1,P;
assume A1:P = { |[ s,t ]|:t1<t };
set t3 =t1+1; t1<t3 by REAL_2:174;
then |[ 0,t3 ]| in { |[ s,t ]|:t1<t };
then P is convex non empty by A1,Th20;
hence thesis by Th9;
end;
theorem Th22:
for t2,P st P = { |[ s,t ]|: t<t2 } holds P is convex
proof let t2,P;
assume A1:P = { |[ s,t ]|:t<t2 };
let w1,w2 such that A2: w1 in P & w2 in P;
let x be set such that A3: x in LSeg(w1,w2);
consider s3,t3 such that
A4:|[ s3,t3 ]|=w1 & t3<t2 by A1,A2;
A5: w1`1=s3 & w1`2=t3 by A4,EUCLID:56;
consider s4,t4 such that
A6:|[ s4,t4 ]|=w2 & t4<t2 by A1,A2;
A7: w2`1=s4 & w2`2=t4 by A6,EUCLID:56;
x in {(1-lambda)*w1 + lambda*w2: 0 <= lambda & lambda <=
1} by A3,TOPREAL1:def 4;
then consider l such that A8: x = (1-l)*w1 + l*w2& 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:59;
(1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| & l*w2=|[ l*w2`1 ,l*w2`2 ]|
by EUCLID:61;
then ((1-l)*w1)`1= (1-l)*w1`1 & ((1-l)*w1)`2= (1-l)*w1`2
& (l*w2)`1=l*w2`1 & (l*w2)`2=l*w2`2 by EUCLID:56;
then w`1=(1-l)* w1`1+ l* w2`1 & w`2=(1-l)* w1`2+ l* w2`2 by A9,EUCLID:56;
then t2> w`2 &
w = |[w`1, w`2]| by A4,A5,A6,A7,A8,Th11,EUCLID:57;
hence thesis by A1,A8;
end;
theorem Th23:
for t2,P st P = { |[ s,t ]|: t<t2 } holds P is connected
proof let t2,P;
assume A1:P = { |[ s,t ]|:t<t2 };
set t3 =t2-1; t3<t2 by REAL_2:174;
then |[ 0,t3 ]| in { |[ s,t ]|:t<t2 };
then P is convex non empty by A1,Th22;
hence thesis by Th9;
end;
theorem Th24:
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<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by Th13;
A2:{ |[ s,t ]|:s<s1} is Subset of TOP-REAL 2 by Lm2,Lm3;
A3:{ |[ s,t ]|:t<t1} is Subset of TOP-REAL 2 by Lm2,Lm4;
A4:{ |[ s,t ]|:s2<s} is Subset of TOP-REAL 2 by Lm2,Lm5;
{ |[ s,t ]|:t2<t} is Subset of TOP-REAL 2 by Lm2,Lm6;
then reconsider A0={ |[ s,t ]|:s<s1}, A1={ |[ s,t ]|:t<t1},
A2={ |[ s,t ]|:s2<s}, A3={ |[ s,t ]|:t2<t}
as Subset of TOP-REAL 2 by A2,A3,A4;
A5:s1-1<s1 by REAL_2:174;A6:t1-1<t1 by REAL_2:174;
A7: |[s1-1,t1-1]| in A0 by A5;
|[s1-1,t1-1]| in A1 by A6;
then A0 /\ A1 <> {} by A7,XBOOLE_0:def 3;
then A8: A0 meets A1 by XBOOLE_0:def 7;
A9: s2< s2+1 by REAL_2:174;
A10:|[s2+1,t1-1]| in A1 by A6;
|[s2+1,t1-1]| in A2 by A9;
then A1 /\ A2 <> {} by A10,XBOOLE_0:def 3;
then A11: A1 meets A2 by XBOOLE_0:def 7;
A12: t2< t2+1 by REAL_2:174;
A13:|[s2+1,t2+1]| in A2 by A9;
|[s2+1,t2+1]| in A3 by A12;
then A2 /\ A3 <> {} by A13,XBOOLE_0:def 3;
then A14: A2 meets A3 by XBOOLE_0:def 7;
A15:A0 is connected by Th19;
A16:A1 is connected by Th23;
A17:A2 is connected by Th17;
A3 is connected by Th21;
hence thesis by A1,A8,A11,A14,A15,A16,A17,Th8;
end;
Lm9: (s-r)^2=(r-s)^2
proof A1:(s-r)^2=s^2-2*s*r + r^2 by SQUARE_1:64
.= r^2+s^2-2*s*r by XCMPLX_1:29
.= r^2+s^2-2*(r*s) by XCMPLX_1:4;
(r-s)^2=r^2-2*r*s + s^2 by SQUARE_1:64
.= r^2+s^2-2*r*s by XCMPLX_1:29
.= r^2+s^2-2*(r*s) by XCMPLX_1:4;
hence thesis by A1;
end;
Lm10: TOP-REAL 2 =TopSpaceMetr(Euclid 2) by EUCLID:def 8;
theorem Th25:
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1<s } holds
P is open
proof let s1; let P be Subset of TOP-REAL 2 such that A1:P= { |[ s,t ]|:s1<s };
for pe being Point of Euclid 2 st pe in P ex r being real number 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 A2:|[ s,t ]|=pe & s1<s by A1;
set r=(s-s1)/2; s-s1>0 by A2,SQUARE_1:11; then A3: r>0 by REAL_2:127;
Ball(pe,r) c= P
proof let x be set; assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r}
by METRIC_1:18;
then consider q being Element of Euclid 2
such that A4: q=x and A5: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by TOPREAL3:13;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then A6: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A5,TOPREAL3:12;
A7: 0 <= (ppe`1 - pq`1)^2 & 0 <= (ppe`2 - pq`2)^2 by SQUARE_1:72;
then A8: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by REAL_1:55;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 4;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A6,SQUARE_1:78;
then A9:(ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A8,SQUARE_1:def 4;
(ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A7,REAL_2:
173
;
then (ppe`1 - pq`1)^2 <r^2 by A9,AXIOMS:22;
then ppe`1 - pq`1 < r by A3,SQUARE_1:77; then ppe`1 <pq`1+r by REAL_1:84
;
then ppe`1 - r < pq`1 by REAL_1:84;
then A10: s-(s-s1)/2 < pq`1 by A2,EUCLID:56;
s-(s-s1)/2 = s-s1+s1-(s-s1)/2 by XCMPLX_1:27
.= (s-s1)-(s-s1)/2+s1 by XCMPLX_1:29
.= (s-s1)/2+(s-s1)/2-(s-s1)/2+s1 by XCMPLX_1:66
.= (s-s1)/2-(s-s1)/2+(s-s1)/2+s1 by XCMPLX_1:29
.=0+(s-s1)/2+s1 by XCMPLX_1:14
.=r+s1;
then s1< s-(s-s1)/2 by A3,REAL_2:174;
then |[pq`1,pq`2]|=x & s1<pq`1 by A4,A10,AXIOMS:22,EUCLID:57;
hence thesis by A1;
end;
hence thesis by A3;
end;
hence thesis by Lm10,TOPMETR:22;
end;
theorem Th26:
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>s } holds
P is open
proof let s1; let P be Subset of TOP-REAL 2 such that
A1:P= { |[ s,t ]|:s1>s };
for pe being Point of Euclid 2 st pe in P ex r being real number 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 A2:|[ s,t ]|=pe & s1>s by A1;
set r=(s1-s)/2; s1-s>0 by A2,SQUARE_1:11; then A3: r>0 by REAL_2:127;
Ball(pe,r) c= P
proof let x be set; assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r}
by METRIC_1:18;
then consider q being Element of Euclid 2
such that A4: q=x and A5: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by TOPREAL3:13;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then A6: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A5,TOPREAL3:12;
A7: 0 <= (ppe`1 - pq`1)^2 & 0 <= (ppe`2 - pq`2)^2 by SQUARE_1:72;
then A8: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by REAL_1:55;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 4;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A6,SQUARE_1:78;
then A9:(ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A8,SQUARE_1:def 4;
(ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A7,REAL_2:
173
;
then (ppe`1 - pq`1)^2 <r^2 by A9,AXIOMS:22;
then (pq`1-ppe`1)^2 <r^2 by Lm9;
then pq`1-ppe`1 < r by A3,SQUARE_1:77;
then ppe`1 + r > pq`1 by REAL_1:84;
then A10: s+(s1-s)/2 > pq`1 by A2,EUCLID:56;
s+(s1-s)/2 = s-s1+s1+(s1-s)/2 by XCMPLX_1:27
.= s-s1 +(s1-s)/2+s1 by XCMPLX_1:1
.=-(s1-s)+(s1-s)/2+s1 by XCMPLX_1:143
.=-((s1-s)/2+(s1-s)/2)+(s1-s)/2+s1 by XCMPLX_1:66
.=-r-r+r+s1 by XCMPLX_1:161 .=-r+r-r+s1 by XCMPLX_1:29
.=0-r+s1 by XCMPLX_0:def 6
.=-r+s1 by XCMPLX_1:150
.=s1-r by XCMPLX_0:def 8;
then s1> s+(s1-s)/2 by A3,REAL_2:174;
then |[pq`1,pq`2]|=x & s1>pq`1 by A4,A10,AXIOMS:22,EUCLID:57;
hence thesis by A1;
end;
hence thesis by A3;
end;
hence thesis by Lm10,TOPMETR:22;
end;
theorem Th27:
for s1 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:s1<t } holds P is open
proof let s1; let P be Subset of TOP-REAL 2 such that
A1:P= { |[ s,t ]|:s1<t };
for pe being Point of Euclid 2 st pe in P ex r being real number
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 A2:|[ s,t ]|=pe & s1<t by A1;
set r=(t-s1)/2; t-s1>0 by A2,SQUARE_1:11; then A3: r>0 by REAL_2:127;
Ball(pe,r) c= P
proof let x be set; assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r}
by METRIC_1:18;
then consider q being Element of Euclid 2
such that A4: q=x and A5: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by TOPREAL3:13;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then A6: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A5,TOPREAL3:12;
A7: 0 <= (ppe`1 - pq`1)^2 & 0 <= (ppe`2 - pq`2)^2 by SQUARE_1:72;
then A8: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by REAL_1:55;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 4;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A6,SQUARE_1:78;
then A9:(ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A8,SQUARE_1:def 4;
(ppe`2 - pq`2)^2 <= (ppe`2 - pq`2)^2+(ppe`1 - pq`1)^2 by A7,REAL_2:173;
then (ppe`2 - pq`2)^2 <r^2 by A9,AXIOMS:22;
then ppe`2 - pq`2 < r by A3,SQUARE_1:77; then ppe`2 <pq`2+r by REAL_1:84
;
then ppe`2 - r < pq`2 by REAL_1:84;
then A10: t-(t-s1)/2 < pq`2 by A2,EUCLID:56;
t-(t-s1)/2 = t-s1+s1-(t-s1)/2 by XCMPLX_1:27
.= (t-s1)-(t-s1)/2+s1 by XCMPLX_1:29
.= (t-s1)/2+(t-s1)/2-(t-s1)/2+s1 by XCMPLX_1:66
.= (t-s1)/2-(t-s1)/2+(t-s1)/2+s1 by XCMPLX_1:29
.=0+(t-s1)/2+s1 by XCMPLX_1:14
.=r+s1;
then s1< t-(t-s1)/2 by A3,REAL_2:174;
then |[pq`1,pq`2]|=x & s1<pq`2 by A4,A10,AXIOMS:22,EUCLID:57;
hence thesis by A1;
end;
hence thesis by A3;
end;
hence thesis by Lm10,TOPMETR:22;
end;
theorem Th28:
for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>t } holds
P is open
proof let s1; let P be Subset of TOP-REAL 2 such that
A1:P= { |[ s,t ]|:s1>t };
for pe being Point of Euclid 2 st pe in P ex r being real number 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 A2:|[ s,t ]|=pe & s1>t by A1;
set r=(s1-t)/2; s1-t>0 by A2,SQUARE_1:11; then A3: r>0 by REAL_2:127;
Ball(pe,r) c= P
proof let x be set; assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r}
by METRIC_1:18;
then consider q being Element of Euclid 2
such that A4: q=x and A5: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by TOPREAL3:13;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then A6: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A5,TOPREAL3:12;
A7: 0 <= (ppe`1 - pq`1)^2 & 0 <= (ppe`2 - pq`2)^2 by SQUARE_1:72;
then A8: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by REAL_1:55;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 4;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A6,SQUARE_1:78;
then A9:(ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A8,SQUARE_1:def 4;
(ppe`2 - pq`2)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A7,REAL_2:
173
;
then (ppe`2 - pq`2)^2 <r^2 by A9,AXIOMS:22;
then (pq`2-ppe`2)^2 <r^2 by Lm9;
then pq`2-ppe`2 < r by A3,SQUARE_1:77;
then ppe`2 + r > pq`2 by REAL_1:84;
then A10: t+(s1-t)/2 > pq`2 by A2,EUCLID:56;
t+(s1-t)/2 = t-s1+s1+(s1-t)/2 by XCMPLX_1:27
.= t-s1 +(s1-t)/2+s1 by XCMPLX_1:1
.=-(s1-t)+(s1-t)/2+s1 by XCMPLX_1:143
.=-((s1-t)/2+(s1-t)/2)+(s1-t)/2+s1 by XCMPLX_1:66
.=-r-r+r+s1 by XCMPLX_1:161 .=-r+r-r+s1 by XCMPLX_1:29
.=0-r+s1 by XCMPLX_0:def 6
.=-r+s1 by XCMPLX_1:150
.=s1-r by XCMPLX_0:def 8;
then s1> t+(s1-t)/2 by A3,REAL_2:174;
then |[pq`1,pq`2]|=x & s1>pq`2 by A4,A10,AXIOMS:22,EUCLID:57;
hence thesis by A1;
end;
hence thesis by A3;
end;
hence thesis by Lm10,TOPMETR:22;
end;
theorem Th29:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} holds P is open
proof let s1,t1,s2,t2; let P be Subset of TOP-REAL 2;
assume A1:P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
{|[s,t]|:s1<s} is Subset of TOP-REAL 2 by Lm2,Lm5;
then reconsider P1={|[s,t]|:s1<s} as Subset of TOP-REAL 2;
{|[s,t]|:s<s2} is Subset of TOP-REAL 2 by Lm2,Lm3;
then reconsider P2={|[s,t]|:s<s2} as Subset of TOP-REAL 2;
{|[s,t]|:t1<t} is Subset of TOP-REAL 2 by Lm2,Lm6;
then reconsider P3={|[s,t]|:t1<t} as Subset of TOP-REAL 2;
{|[s,t]|:t<t2} is Subset of TOP-REAL 2 by Lm2,Lm4;
then reconsider P4={|[s,t]|:t<t2} as Subset of TOP-REAL 2;
A2: P=P1 /\ P2 /\ P3 /\ P4 by A1,Th12;
P1 is open & P2 is open by Th25,Th26;
then A3: P1 /\ P2 is open by TOPS_1:38;
A4: P3 is open & P4 is open by Th27,Th28;
then P1 /\ P2 /\ P3 is open by A3,TOPS_1:38;
hence thesis by A2,A4,TOPS_1:38;
end;
theorem Th30:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} holds P is open
proof let s1,t1,s2,t2; let P be Subset of TOP-REAL 2; assume
P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
then A1: P={ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by Th13;
{ |[ s,t ]|:s<s1} is Subset of TOP-REAL 2 by Lm2,Lm3;
then reconsider A0={ |[ s,t ]|:s<s1} as Subset of TOP-REAL 2;
{ |[ s,t ]|:t<t1} is Subset of TOP-REAL 2 by Lm2,Lm4;
then reconsider A1={ |[ s,t ]|:t<t1} as Subset of TOP-REAL 2;
{ |[ s,t ]|:s2<s} is Subset of TOP-REAL 2 by Lm2,Lm5;
then reconsider A2={ |[ s,t ]|:s2<s} as Subset of TOP-REAL 2;
{ |[ s,t ]|:t2<t} is Subset of TOP-REAL 2 by Lm2,Lm6;
then reconsider A3={ |[ s,t ]|:t2<t} as Subset of TOP-REAL 2;
A0 is open & A1 is open by Th26,Th28;
then A2: A0 \/ A1 is open by TOPS_1:37;
A2 is open by Th25; then A3: A0 \/ A1 \/ A2 is open by A2,TOPS_1:37;
A3 is open by Th27;
hence thesis by A1,A3,TOPS_1:37;
end;
theorem Th31:
for s1,t1,s2,t2,P,Q st
P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} &
Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} holds
P misses Q
proof let s1,t1,s2,t2,P,Q;
assume that
A1: P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} and
A2: Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
assume not thesis;
then consider x be set such that
A3: x in P & x in Q by XBOOLE_0:3;
consider sa,ta such that A4:|[sa,ta]|=x
and A5: (s1<sa & sa<s2 & t1<ta & ta<t2) by A1,A3;
consider sb,tb such that A6:|[sb,tb]|=x
and A7:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2) by A2,A3;
set p= |[sa,ta]|;
p`1=sa & p`1=sb & p`2=ta & p`2=tb by A4,A6,EUCLID:56;
hence contradiction by A5,A7;
end;
theorem Th32:
for s1,s2,t1,t2 be Real holds
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} =
{|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2}
proof let s1,s2,t1,t2;
now let x be set;
A1: now assume x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2};
then consider pp being Point of TOP-REAL 2
such that A2:pp=x & s1<pp`1 & pp`1<s2 & t1<pp`2 & pp`2<t2;
|[pp`1,pp`2]|=x & s1<pp`1 & pp`1<s2 & t1<pp`2 & pp`2<t2
by A2,EUCLID:57;
hence x in {|[s1a,t1a]|:s1<s1a & s1a<s2 & t1<t1a & t1a<t2};
end;
now assume x in {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2};
then consider sa,ta being Real such that
A3: |[sa,ta]|=x &
(s1<sa & sa<s2 & t1<ta & ta<t2);
set pa=|[sa,ta]|;
pa=x &
(s1<pa`1 & pa`1<s2 & t1<pa`2 & pa`2<t2) by A3,EUCLID:56;
hence x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2};
end;hence x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2}
iff x in {|[sa,ta]|:s1<sa & sa<s2 &
t1<ta & ta<t2} by A1;end;
hence thesis by TARSKI:2;
end;
theorem Th33:
for s1,s2,t1,t2 holds
{qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} =
{|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
proof let s1,s2,t1,t2;
now let x be set;
A1: now assume x in
{qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
then consider q being Point of TOP-REAL 2 such that A2:q=x &
not (s1<=q`1 & q`1<=s2 & t1<=q`2 & q`2<=t2);
|[q`1,q`2]|=x & not (s1<=q`1 & q`1<=s2 & t1<=q`2 & q`2<=t2)
by A2,EUCLID:57;
hence x in {|[s2a,t2a]| :
not (s1<=s2a & s2a<=s2 & t1<=t2a & t2a<=t2)};
end;
now assume x in {|[sb,tb]| :
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
then consider sb,tb being Real such that
A3: |[sb,tb]|=x &
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2);
set qa=|[sb,tb]|;
qa=x & not (s1<=qa`1 & qa`1<=s2 & t1<=qa`2 & qa`2<=t2)
by A3,EUCLID:56;
hence x in {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
end;
hence x in
{qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)}
iff x in {|[sb,tb]| :
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th34:
for s1,s2,t1,t2 holds
{ p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2 & t1<p0`2 & p0`2<t2}
is Subset of TOP-REAL 2
proof let s1,s2,t1,t2;
{ |[ sc,tc ]|: s1<sc & sc<s2 & t1<tc & tc<t2}
is Subset of TOP-REAL 2 by Lm2,Lm7;
hence thesis by Th32;
end;
theorem Th35:
for s1,s2,t1,t2 holds
{ pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)}
is Subset of TOP-REAL 2
proof let s1,s2,t1,t2;
{ |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
is Subset of TOP-REAL 2 by Lm2,Lm8;
hence thesis by Th33;
end;
theorem Th36:
for s1,t1,s2,t2,P st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is connected
proof let s1,t1,s2,t2,P;assume
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2};
then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th32;
hence thesis by Th15;
end;
theorem Th37:
for s1,t1,s2,t2,P st
P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is connected
proof let s1,t1,s2,t2,P;assume
P= { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th33;
hence thesis by Th24;
end;
theorem Th38:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is open
proof let s1,t1,s2,t2; let P be Subset of TOP-REAL 2; assume
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2};
then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th32;
hence thesis by Th29;
end;
theorem Th39:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is open
proof let s1,t1,s2,t2; let P be Subset of TOP-REAL 2;assume
P= { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th33;
hence thesis by Th30;
end;
theorem Th40:
for s1,t1,s2,t2,P,Q st
P = {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} &
Q = {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)}
holds P misses Q
proof let s1,t1,s2,t2,P,Q;
assume that A1: P=
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} and
A2:Q=
{qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
A3:P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by A1,Th32;
Q= {|[sb,tb]| :
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A2,Th33;
hence thesis by A3,Th31;
end;
theorem Th41:
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P`= P1 \/ P2 & P`<> {} & P1 misses P2 &
for P1A,P2B being Subset of (TOP-REAL 2)|P`
st P1A = P1 & P2B = P2 holds
P1A is_a_component_of (TOP-REAL 2)|P` & P2B is_a_component_of (TOP-REAL 2)|P`
proof let s1,t1,s2,t2; let P,P1,P2 be Subset of TOP-REAL 2;
assume that A1:s1<s2 & t1<t2 and
A2: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}
and A3: P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2}
and A4: P2 = {pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)};
now let x be set;assume A5: x in P`;
then x in P`;
then x in [#](TOP-REAL 2) \ P by PRE_TOPC:17;
then A6:x in [#](TOP-REAL 2) & not x in P by XBOOLE_0:def 4;
reconsider pd=x as Point of TOP-REAL 2 by A5;
not (pd`1 = s1 & pd`2 <= t2 & pd`2 >= 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 A2,A6;
then s1<pd`1 & pd`1<s2 & t1 <pd`2 & pd`2 < t2
or not( s1<=pd`1 & pd`1<=s2 & t1<=pd`2 & pd`2<=t2) by REAL_1:def 5;
then x in P1 or x in P2 by A3,A4;hence x in P1 \/ P2 by XBOOLE_0:def 2
;
end; then A7:P` c= P1 \/ P2 by TARSKI:def 3;
now let x be set such that A8: x in P1 \/ P2;
now per cases by A8,XBOOLE_0:def 2;
suppose A9: x in P1;
then A10: ex pa st pa=x
& s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A3;
now assume x in P;
then ex pb st pb=x &(pb`1 = s1 & pb`2 <= t2 & pb`2 >= 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 A2;
hence contradiction by A10;
end;
hence x in P` by A9,SUBSET_1:50;
suppose x in P2;
then consider pc being Point of TOP-REAL 2 such that A11:pc=x and
A12: not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2) by A4;
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 A2;
hence contradiction by A1,A12;
end;
hence x in P`by A11,SUBSET_1:50;
end;
hence x in P`;
end; then P1 \/ P2 c= P` by TARSKI:def 3;
hence A13: P`=P1 \/ P2 by A7,XBOOLE_0:def 10;
set s3 =(s1+s2)/2, t3=(t1+t2)/2;
s1+s1<s1+s2 & t1+t1<t1+t2 by A1,REAL_1:53;
then (s1+s1)/2<s3 & (t1+t1)/2<t3 by REAL_1:73;
then A14: s1<s3 & t1<t3 by XCMPLX_1:65;
s1+s2<s2+s2 & t1+t2<t2+t2 by A1,REAL_1:53;
then s3<(s2+s2)/2 & t3<(t2+t2)/2 by REAL_1:73;
then A15: s3<s2 & t3<t2 by XCMPLX_1:65;
set pp=|[s3,t3]|;
pp`1=s3 & pp`2=t3 by EUCLID:56;
then A16: |[ s3,t3 ]| in { pp2 where pp2 is Point of TOP-REAL 2:
s1<pp2`1 & pp2`1<s2 & t1<pp2`2 & pp2`2<t2} by A14,A15;
then consider x be set such that A17:x in P1 by A3;
thus
P`<>{} by A13,A17,XBOOLE_0:def 2;
set P' = P`;
P1 misses P2 by A3,A4,Th40;
hence A18: P1 /\ P2 = {} by XBOOLE_0:def 7;
now let P1A,P2B be Subset of (TOP-REAL 2)|P';
assume A19: P1A=P1 & P2B=P2;
P1 is connected by A3,Th36;
then A20: P1A is connected by A19,CONNSP_1:24;
A21:P2 is connected by A4,Th37;
A22: P2={ |[ sa,ta ]|:not (s1<=sa & sa<=s2 &
t1<=ta & ta<=t2)} by A4,Th33;
reconsider A0={ |[ s3a,t3a ]|:s3a<s1}
as Subset of TOP-REAL 2 by Lm2,Lm3;
reconsider A1={ |[ s4,t4 ]|:t4<t1} as Subset of TOP-REAL 2
by Lm2,Lm4;
reconsider A2={ |[ s5,t5 ]|:s2<s5} as Subset of TOP-REAL 2
by Lm2,Lm5;
reconsider A3={ |[ s6,t6 ]|:t2<t6} as Subset of TOP-REAL 2
by Lm2,Lm6;
A23: P2=A0 \/ A1 \/ A2 \/ A3 by A22,Th13; t2+1>t2 by REAL_2:174;
then |[s2+1,t2+1]| in A3;
then A24: P2B <>{} by A19,A23,XBOOLE_1:15;
A25: P2B is connected by A19,A21,CONNSP_1:24;
A26: for CP being Subset of (TOP-REAL 2)|(P') st
CP is connected holds P1A c= CP implies P1A = CP
proof let CP be Subset of (TOP-REAL 2)|(P');
assume CP is connected;
then A27:((TOP-REAL 2)|P')|CP is connected by CONNSP_1:def 3;
now assume A28:P1A c= CP;
P1A /\ CP c= the carrier of ((TOP-REAL 2)|P')|CP
proof P1A /\ CP c= CP by XBOOLE_1:17;
hence thesis by Th1;
end;
then reconsider AP=P1A /\ CP
as Subset of ((TOP-REAL 2)|P')|CP;
A29: P1 /\ P` =P1A by A13,A19,XBOOLE_1:21; P1 is open by A3,Th38;
then A30: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 5;
A31: P`= [#]((TOP-REAL 2)|P') by PRE_TOPC:def 10;
P1 /\ [#]((TOP-REAL 2)|P')=P1A by A29,PRE_TOPC:def 10;
then A32: P1A in the topology of (TOP-REAL 2)|P' by A30,PRE_TOPC:def 9;
A33: CP=[#](((TOP-REAL 2)|P')|CP) by PRE_TOPC:def 10;
A34:AP<>{}(((TOP-REAL 2)|P')|CP) by A3,A16,A19,A28,XBOOLE_1:28;
AP in the topology of ((TOP-REAL 2)|P')|CP by A32,A33,PRE_TOPC:def 9;
then A35:AP is open by PRE_TOPC:def 5;
P2B /\ CP c= the carrier of ((TOP-REAL 2)|P')|CP
proof P2B /\ CP c= CP by XBOOLE_1:17;
hence thesis by Th1;
end;
then reconsider BP=P2B /\ CP
as Subset of ((TOP-REAL 2)|P')|CP;
A36: P2 /\ P` =P2B by A13,A19,XBOOLE_1:21; P2 is open by A4,Th39;
then A37: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 5;
P2 /\ [#]((TOP-REAL 2)|P')=P2B by A36,PRE_TOPC:def 10;
then A38: P2B in the topology of (TOP-REAL 2)|P' by A37,PRE_TOPC:def 9;
CP=[#](((TOP-REAL 2)|P')|CP) by PRE_TOPC:def 10;
then BP in the topology of ((TOP-REAL 2)|P')|CP by A38,PRE_TOPC:def 9;
then A39:BP is open by PRE_TOPC:def 5;
CP c= P` by A31,PRE_TOPC:14;
then A40: CP=(P1A \/ P2B) /\ CP by A13,A19,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now assume A41: BP<>{};
A42: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 A3,A4,Th40;
then P1 /\ P2 = {} by XBOOLE_0:def 7;
then AP misses BP by A19,A42,XBOOLE_0:def 7;
hence contradiction by A27,A33,A34,A35,A39,A40,A41,CONNSP_1:12;
end;
hence thesis by A40,XBOOLE_1:28;
end;
hence thesis;
end;
hence P1A is_a_component_of (TOP-REAL 2)|P' by A20,CONNSP_1:def 5;
for CP being Subset of (TOP-REAL 2)|(P') st
CP is connected holds P2B c= CP implies P2B = CP
proof let CP be Subset of (TOP-REAL 2)|(P');
assume CP is connected;
then A43:((TOP-REAL 2)|P')|CP is connected by CONNSP_1:def 3;
assume A44:P2B c= CP;
P2B /\ CP c= the carrier of ((TOP-REAL 2)|P')|CP
proof P2B /\ CP c= CP by XBOOLE_1:17;
hence thesis by Th1;
end;
then reconsider BP=P2B /\ CP
as Subset of ((TOP-REAL 2)|P')|CP;
A45: P2 /\ P` =P2B by A13,A19,XBOOLE_1:21; P2 is open by A4,Th39;
then A46: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 5;
A47: P`= [#]((TOP-REAL 2)|P') by PRE_TOPC:def 10;
P2 /\ [#]((TOP-REAL 2)|P')=P2B by A45,PRE_TOPC:def 10;
then A48: P2B in the topology of (TOP-REAL 2)|P' by A46,PRE_TOPC:def 9;
A49: CP=[#](((TOP-REAL 2)|P')|CP) by PRE_TOPC:def 10;
A50:BP<>{}(((TOP-REAL 2)|P')|CP) by A24,A44,XBOOLE_1:28;
BP in the topology of ((TOP-REAL 2)|P')|CP by A48,A49,PRE_TOPC:def 9;
then A51:BP is open by PRE_TOPC:def 5;
P1A /\ CP c= the carrier of ((TOP-REAL 2)|P')|CP
proof P1A /\ CP c= CP by XBOOLE_1:17;
hence thesis by Th1;
end;
then reconsider AP=P1A /\ CP
as Subset of ((TOP-REAL 2)|P')|CP;
A52: P1 /\ P` =P1A by A13,A19,XBOOLE_1:21; P1 is open by A3,Th38;
then A53: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 5;
P1 /\ [#]((TOP-REAL 2)|P')=P1A by A52,PRE_TOPC:def 10;
then A54: P1A in the topology of (TOP-REAL 2)|P' by A53,PRE_TOPC:def 9;
CP=[#](((TOP-REAL 2)|P')|CP) by PRE_TOPC:def 10;
then AP in the topology of ((TOP-REAL 2)|P')|CP by A54,PRE_TOPC:def 9;
then A55:AP is open by PRE_TOPC:def 5;
CP c= P` by A47,PRE_TOPC:14;
then A56: CP=(P1A \/ P2B) /\ CP by A13,A19,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now assume A57: 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 A18,A19,XBOOLE_0:def 7;
hence contradiction by A43,A49,A50,A51,A55,A56,A57,CONNSP_1:12;
end;
hence thesis by A44,A56,XBOOLE_1:28;
end;
hence P1A is_a_component_of (TOP-REAL 2)|P' &
P2B is_a_component_of (TOP-REAL 2)|P'
by A20,A25,A26,CONNSP_1:def 5;
end;
hence thesis;
end;
theorem Th42:
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds P = (Cl P1) \ P1 & P = (Cl P2) \P2
proof let s1,t1,s2,t2; let P,P1,P2 be Subset of TOP-REAL 2;
assume that A1: s1<s2 & t1<t2 and
A2: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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2}
& P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)};
reconsider PP = P` as Subset of TOP-REAL 2;
A3: PP=P1 \/ P2 & PP <> {} & P1 misses P2 by A1,A2,Th41;
then A4:P2 c= P1` & P1 c= P2` by PRE_TOPC:21;
P= (P1 \/ P2)` by A3;
then P=[#](TOP-REAL 2) \ (P1 \/ P2) by PRE_TOPC:17;
then A5:P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
then P c=[#](TOP-REAL 2)\P2 by XBOOLE_1:17;
then P c= P2` by PRE_TOPC:17;
then A6:P c= P2`;
A7:[#](TOP-REAL 2)=P \/ (P2 \/ P1) by A3,PRE_TOPC:18
.=P \/ P2 \/ P1 by XBOOLE_1:4;
A8: P1`= P \/ P2
proof
now let x be set;assume x in P1`;
then x in P1`;
then x in [#](TOP-REAL 2)\P1 by PRE_TOPC:17;
then x in [#](TOP-REAL 2) & not x in P1 by XBOOLE_0:def 4;
hence x in P \/ P2 by A7,XBOOLE_0:def 2;
end; then A9:P1` c=P \/ P2 by TARSKI:def 3;
now let x be set;assume x in P \/ P2;
then x in P or x in P2 by XBOOLE_0:def 2;
then x in [#](TOP-REAL 2)\P1 or x in P2 by A5,XBOOLE_0:def 3;
then x in P1` by A4,PRE_TOPC:17;
hence x in P1`;
end; then P \/ P2 c=P1` by TARSKI:def 3;
hence thesis by A9,XBOOLE_0:def 10;
end;
A10:P1 is open by A2,Th38;
[#](TOP-REAL 2) \ P1` = P1`` by PRE_TOPC:17
.=P1;
then A11: P \/ P2 is closed by A8,A10,PRE_TOPC:def 6;
A12:P2 c= P \/ P2 by XBOOLE_1:7;
Cl P2 c= P \/ P2
proof let x be set;assume x in Cl P2;
hence thesis by A11,A12,PRE_TOPC:45;
end;
then A13:(Cl P2) \ P2 c= P \/ P2 \P2 by XBOOLE_1:33;
(P \/ P2) \ P2 c= P
proof let x be set;assume x in (P \/ P2) \ P2;
then x in P \/ P2 & not x in P2 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 2;
end;
then A14:(Cl P2)\P2 c= P by A13,XBOOLE_1:1;
A15: P c= (Cl P2)\P2
proof
P c= Cl P2
proof let x be set;assume x in P;
then consider p being Point of TOP-REAL 2 such that
A16:p=x and
A17: 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 A2;
reconsider q=p as Point of Euclid 2 by TOPREAL3:13;
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;
consider r be real number such that A21: r>0 and
A22:Ball(q,r) c= Q by A19,A20,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
set pa=|[p`1-r/2,p`2]|;
A23:pa`1=p`1-r/2 & pa`2=p`2 by EUCLID:56;
A24: r/2>0 by A21,SEQ_2:3;
then not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A18,A23,
REAL_2:174;
then A25:pa in P2 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A26: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A27:(p`2 - pa`2)^2 =0 by A23,SQUARE_1:60,XCMPLX_1:14;
A28: p`1-pa`1 = r/2 by A23,XCMPLX_1:18;
then p`1 - pa`1 < r by A21,SEQ_2:4;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A24,A27,A28,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A26,SQUARE_1:def 4;
then A29:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A21,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A29,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
then P2 /\ Q <> {} by A22,A25,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 7;
end;
hence x in Cl P2 by A16,PRE_TOPC:def 13;
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;
consider r being real number such that
A33: r>0 and A34:Ball(q,r) c= Q by A31,A32,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
set pa=|[p`1,p`2+r/2]|;
A35:pa`1=p`1 & pa`2=p`2+r/2 by EUCLID:56;
A36: r/2>0 by A33,SEQ_2:3;
then not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A30,A35,
REAL_2:174;
then A37:pa in P2 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A38: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A39:(p`1 - pa`1)^2 =0 by A35,SQUARE_1:60,XCMPLX_1:14;
A40: pa`2-p`2 = r/2 by A35,XCMPLX_1:26;
then A41:pa`2 - p`2 < r by A33,SEQ_2:4;
(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A36,A39,A40,A41,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A38,SQUARE_1:def 4;
then A42:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A33,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A42,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
then P2 /\ Q <> {} by A34,A37,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 7;
end;
hence x in Cl P2 by A16,PRE_TOPC:def 13;
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;
consider r being real number such that
A46: r>0 and A47:Ball(q,r) c= Q by A44,A45,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
set pa=|[p`1,p`2-r/2]|;
A48:pa`1=p`1 & pa`2=p`2-r/2 by EUCLID:56;
A49: r/2>0 by A46,SEQ_2:3;
then not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A43,A48,REAL_2:174;
then A50:pa in P2 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A51: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A52:(p`1 - pa`1)^2 =0 by A48,SQUARE_1:60,XCMPLX_1:14;
A53: p`2-pa`2 = r/2 by A48,XCMPLX_1:18;
then p`2 - pa`2 < r by A46,SEQ_2:4;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A49,A52,A53,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A51,SQUARE_1:def 4;
then A54:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A46,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A54,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A47,A50,XBOOLE_0:3;
end;
hence x in Cl P2 by A16,PRE_TOPC:def 13;
suppose A55: 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 P2 meets Q
proof let Q be Subset of TOP-REAL 2;assume that
A56:Q is open and A57:p in Q;
consider r being real number such that A58: r>0 and
A59:Ball(q,r) c= Q by A56,A57,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
set pa=|[p`1+r/2,p`2]|;
A60:pa`1=p`1+r/2 & pa`2=p`2 by EUCLID:56;
A61: r/2>0 by A58,SEQ_2:3;
then not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A55,A60,REAL_2:174;
then A62:pa in P2 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A63: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A64:(p`2 - pa`2)^2 =0 by A60,SQUARE_1:60,XCMPLX_1:14;
A65: pa`1-p`1 = r/2 by A60,XCMPLX_1:26;
then A66:pa`1 - p`1 < r by A58,SEQ_2:4;
(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A61,A64,A65,A66,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A63,SQUARE_1:def 4;
then A67:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A58,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A67,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A59,A62,XBOOLE_0:3;
end;
hence x in Cl P2 by A16,PRE_TOPC:def 13;
end;
hence x in Cl P2;
end;
then P c= Cl P2 /\ P2` by A6,XBOOLE_1:19;
hence thesis by SUBSET_1:32;
end;
P c=[#](TOP-REAL 2)\P1 by A5,XBOOLE_1:17;
then P c= P1` by PRE_TOPC:17;
then A68:P c= P1`;
[#](TOP-REAL 2)=P \/ (P1 \/ P2) by A3,PRE_TOPC:18;
then A69:[#](TOP-REAL 2)=P \/ P1 \/ P2 by XBOOLE_1:4;
A70: P2`= P \/ P1
proof
now let x be set;assume x in P2`;
then x in P2`;
then x in [#](TOP-REAL 2)\P2 by PRE_TOPC:17;
then x in [#](TOP-REAL 2) & not x in P2 by XBOOLE_0:def 4;
hence x in P \/ P1 by A69,XBOOLE_0:def 2;
end; then A71:P2` c=P \/ P1 by TARSKI:def 3;
now let x be set;assume x in P \/ P1;
then x in P or x in P1 by XBOOLE_0:def 2;
then x in [#](TOP-REAL 2)\P2 or x in P1 by A5,XBOOLE_0:def 3;
then x in P2` by A4,PRE_TOPC:17;
hence x in P2`;
end; then P \/ P1 c=P2` by TARSKI:def 3;
hence thesis by A71,XBOOLE_0:def 10;
end;
A72:P2 is open by A2,Th39;
[#](TOP-REAL 2) \ P2` = P2`` by PRE_TOPC:17
.=P2;
then A73: P \/ P1 is closed by A70,A72,PRE_TOPC:def 6;
A74:P1 c= P \/ P1 by XBOOLE_1:7;
Cl P1 c= P \/ P1
proof let x be set;assume x in Cl P1;
hence thesis by A73,A74,PRE_TOPC:45;
end;
then A75:(Cl P1) \ P1 c= P \/ P1 \P1 by XBOOLE_1:33;
(P \/ P1) \ P1 c= P
proof let x be set;assume x in (P \/ P1) \ P1;
then x in P \/ P1 & not x in P1 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 2;
end;
then A76:(Cl P1)\P1 c= P by A75,XBOOLE_1:1;
P c= (Cl P1)\P1
proof
P c= Cl P1
proof let x be set;assume x in P;
then consider p being Point of TOP-REAL 2 such that
A77:p=x and
A78: 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 A2;
reconsider q=p as Point of Euclid 2 by TOPREAL3:13;
now per cases by A78;
suppose A79: p`1 = s1 & p`2 <= t2 & p`2 >= t1;
now per cases by A79,REAL_1:def 5;
suppose A80: 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
A81:Q is open and A82:p in Q;
consider r be real number such that
A83: r>0 and A84:Ball(q,r) c= Q by A81,A82,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A85:r/2>0 by A83,SEQ_2:3;
A86:r/2<r by A83,SEQ_2:4;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A87:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A88:r2<= r/2 & r2<=(s2-s1)/2 & r2<=(t2-t1)/2 by A87,AXIOMS:22;
A89:r2<r by A86,A87,AXIOMS:22;
A90: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A91:0<r2 by A85,SQUARE_1:38;
set pa=|[p`1+r2,p`2]|;
A92:pa`1=p`1+r2 & pa`2=p`2 by EUCLID:56;
(s2-s1)/2<s2-s1 by A90,SEQ_2:4;
then r2<s2-p`1 by A80,A88,AXIOMS:22;
then s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A80,A91,A92,REAL_1:
86,REAL_2:174;
then A93:pa in P1 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A94: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A95:(p`2 - pa`2)^2 =0 by A92,SQUARE_1:60,XCMPLX_1:14;
A96: pa`1-p`1 = r2 by A92,XCMPLX_1:26;
(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A89,A91,A95,A96,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A94,SQUARE_1:def 4;
then A97:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A83,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A97,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A84,A93,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A98: p`1 = s1 & 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
A99:Q is open and A100:p in Q;
consider r be real number such that A101: r>0 and
A102:Ball(q,r) c= Q by A99,A100,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A103:r/2>0 by A101,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A104:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A105: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A106:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A104,AXIOMS:22;
A107: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A108:0<r2 by A103,SQUARE_1:38;
set pa=|[p`1+r2,p`2+r2]|;
A109:pa`1=p`1+r2 & pa`2=p`2+r2 by EUCLID:56;
then A110:pa`1> s1 by A98,A108,REAL_2:174;
A111:pa`2> t1 by A98,A108,A109,REAL_2:174;
(s2-s1)/2<s2-s1 by A107,SEQ_2:4;
then r2<s2-p`1 by A98,A106,AXIOMS:22;
then A112: pa`1<s2 by A109,REAL_1:86;
(t2-t1)/2<t2-t1 by A107,SEQ_2:4;
then r2<t2-p`2 by A98,A106,AXIOMS:22;
then pa`2<t2 by A109,REAL_1:86;
then A113:pa in P1 by A2,A110,A111,A112;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A114: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A115: pa`1-p`1 = r2 by A109,XCMPLX_1:26;
(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
then A116: (p`1 - pa`1)^2 <= (r/2)^2 by A105,A108,A115,SQUARE_1:77;
A117: pa`2-p`2 = r2 by A109,XCMPLX_1:26;
A118:(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
(pa`2-p`2)^2<=(r/2)^2 by A105,A108,A117,SQUARE_1:77;
then A119:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A116,A118,REAL_1:55;
A120:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A103,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A103,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A120,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A119,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A114,SQUARE_1:def 4;
then A121:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A101,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A121,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A102,A113,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A122: p`1 = s1 & p`2 = t2;
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
A123:Q is open and A124:p in Q;
consider r be real number such that
A125: r>0 and A126:Ball(q,r) c= Q by A123,A124,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A127:r/2>0 by A125,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A128:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A129: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A130:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A128,AXIOMS:22;
A131: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A132:0<r2 by A127,SQUARE_1:38;
set pa=|[p`1+r2,p`2-r2]|;
A133:pa`1=p`1+r2 & pa`2=p`2-r2 by EUCLID:56;
then A134:pa`1> s1 by A122,A132,REAL_2:174;
A135:pa`2< t2 by A122,A132,A133,REAL_2:174;
(s2-s1)/2<s2-s1 by A131,SEQ_2:4;
then r2<s2-p`1 by A122,A130,AXIOMS:22;
then A136: pa`1<s2 by A133,REAL_1:86;
(t2-t1)/2<t2-t1 by A131,SEQ_2:4;
then r2<p`2-t1 by A122,A130,AXIOMS:22;
then pa`2>t1 by A133,REAL_2:165;
then A137:pa in P1 by A2,A134,A135,A136;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A138: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A139: pa`1-p`1 = r2 by A133,XCMPLX_1:26;
A140:(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
A141:r2^2<= (r/2)^2 by A129,A132,SQUARE_1:77;
p`2-pa`2 =r2 by A133,XCMPLX_1:18;
then A142:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A139,A140,A141,REAL_1:55;
A143:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A127,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A127,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A143,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A142,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A138,SQUARE_1:def 4;
then A144:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A125,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A144,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A126,A137,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
end;
hence x in Cl P1 by A77;
suppose A145: p`1 <= s2 & p`1 >= s1 & p`2 = t2;
now per cases by A145,REAL_1:def 5;
suppose A146: 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
A147:Q is open and A148:p in Q;
consider r be real number such that
A149: r>0 and A150:Ball(q,r) c= Q by A147,A148,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A151:r/2>0 by A149,SEQ_2:3;
A152:r/2<r by A149,SEQ_2:4;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A153:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A154:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A153,AXIOMS:22;
A155:r2<r by A152,A153,AXIOMS:22;
A156: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A157:0<r2 by A151,SQUARE_1:38;
set pa=|[p`1,p`2-r2]|;
A158:pa`1=p`1 & pa`2=p`2-r2 by EUCLID:56;
(t2-t1)/2<t2-t1 by A156,SEQ_2:4;
then r2<p`2-t1 by A146,A154,AXIOMS:22;
then s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A146,A157,A158,
REAL_2:165,174;
then A159:pa in P1 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A160: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A161:(p`1 - pa`1)^2 =0 by A158,SQUARE_1:60,XCMPLX_1:14;
p`2-pa`2 =r2 by A158,XCMPLX_1:18;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A155,A157,A161,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A160,SQUARE_1:def 4;
then A162:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A149,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A162,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A150,A159,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A163: p`2 = t2 & 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
A164:Q is open and A165:p in Q;
consider r be real number such that
A166: r>0 and A167:Ball(q,r) c= Q by A164,A165,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A168:r/2>0 by A166,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A169:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A170: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A171:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A169,AXIOMS:22;
A172: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A173:0<r2 by A168,SQUARE_1:38;
set pa=|[p`1+r2,p`2-r2]|;
A174:pa`1=p`1+r2 & pa`2=p`2-r2 by EUCLID:56;
then A175:pa`1> s1 by A163,A173,REAL_2:174;
A176:pa`2< t2 by A163,A173,A174,REAL_2:174;
(t2-t1)/2<t2-t1 by A172,SEQ_2:4;
then r2<p`2-t1 by A163,A171,AXIOMS:22;
then A177: pa`2>t1 by A174,REAL_2:165;
(s2-s1)/2<s2-s1 by A172,SEQ_2:4;
then r2<s2-p`1 by A163,A171,AXIOMS:22;
then pa`1<s2 by A174,REAL_1:86;
then A178:pa in P1 by A2,A175,A176,A177;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A179: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
p`2-pa`2 = r2 by A174,XCMPLX_1:18;
then A180: (p`2 - pa`2)^2 <= (r/2)^2 by A170,A173,SQUARE_1:77;
A181: pa`1-p`1 = r2 by A174,XCMPLX_1:26;
A182:(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
(pa`1-p`1)^2<=(r/2)^2 by A170,A173,A181,SQUARE_1:77;
then A183:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A180,A182,REAL_1:55;
A184:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A168,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A168,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A184,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A183,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A179,SQUARE_1:def 4;
then A185:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A166,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A185,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A167,A178,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A186: p`2 = t2 & p`1 = s2;
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
A187:Q is open and A188:p in Q;
consider r be real number such that
A189: r>0 and A190:Ball(q,r) c= Q by A187,A188,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A191:r/2>0 by A189,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A192:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A193: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A194:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A192,AXIOMS:22;
A195: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A196:0<r2 by A191,SQUARE_1:38;
set pa=|[p`1-r2,p`2-r2]|;
A197:pa`1=p`1-r2 & pa`2=p`2-r2 by EUCLID:56;
then A198:pa`1< s2 by A186,A196,REAL_2:174;
A199:pa`2< t2 by A186,A196,A197,REAL_2:174;
(s2-s1)/2<s2-s1 by A195,SEQ_2:4;
then r2<p`1-s1 by A186,A194,AXIOMS:22;
then A200: pa`1>s1 by A197,REAL_2:165;
(t2-t1)/2<t2-t1 by A195,SEQ_2:4;
then r2<p`2-t1 by A186,A194,AXIOMS:22;
then pa`2>t1 by A197,REAL_2:165;
then A201:pa in P1 by A2,A198,A199,A200;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A202: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A203: p`1-pa`1 = r2 by A197,XCMPLX_1:18;
A204:r2^2<= (r/2)^2 by A193,A196,SQUARE_1:77;
p`2-pa`2 =r2 by A197,XCMPLX_1:18;
then A205:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A203,A204,REAL_1:55;
A206:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A191,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A191,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A206,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A205,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A202,SQUARE_1:def 4;
then A207:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A189,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A207,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A190,A201,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
end;
hence x in Cl P1 by A77;
suppose A208: p`1 <= s2 & p`1 >= s1 & p`2 = t1;
now per cases by A208,REAL_1:def 5;
suppose A209: 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
A210:Q is open and A211:p in Q;
consider r be real number such that
A212: r>0 and A213:Ball(q,r) c= Q by A210,A211,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A214:r/2>0 by A212,SEQ_2:3;
A215:r/2<r by A212,SEQ_2:4;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A216:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A217:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A216,AXIOMS:22;
A218:r2<r by A215,A216,AXIOMS:22;
A219: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A220:0<r2 by A214,SQUARE_1:38;
set pa=|[p`1,p`2+r2]|;
A221:pa`2=p`2+r2 & pa`1=p`1 by EUCLID:56;
(t2-t1)/2<t2-t1 by A219,SEQ_2:4;
then r2<t2-p`2 by A209,A217,AXIOMS:22;
then s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A209,A220,A221,
REAL_1:86,REAL_2:174;
then A222:pa in P1 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A223: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A224:(p`1 - pa`1)^2 =0 by A221,SQUARE_1:60,XCMPLX_1:14;
A225: pa`2-p`2 = r2 by A221,XCMPLX_1:26;
(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A218,A220,A224,A225,
SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A223,SQUARE_1:def 4;
then A226:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A212,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A226,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A213,A222,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A227: p`2 = t1 & 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
A228:Q is open and A229:p in Q;
consider r be real number such that
A230: r>0 and A231:Ball(q,r) c= Q by A228,A229,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A232:r/2>0 by A230,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A233:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A234: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A235:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A233,AXIOMS:22;
A236: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A237:0<r2 by A232,SQUARE_1:38;
set pa=|[p`1+r2,p`2+r2]|;
A238:pa`1=p`1+r2 & pa`2=p`2+r2 by EUCLID:56;
then A239:pa`1> s1 by A227,A237,REAL_2:174;
A240:pa`2> t1 by A227,A237,A238,REAL_2:174;
(s2-s1)/2<s2-s1 by A236,SEQ_2:4;
then r2<s2-p`1 by A227,A235,AXIOMS:22;
then A241: pa`1<s2 by A238,REAL_1:86;
(t2-t1)/2<t2-t1 by A236,SEQ_2:4;
then r2<t2-p`2 by A227,A235,AXIOMS:22;
then pa`2<t2 by A238,REAL_1:86;
then A242:pa in P1 by A2,A239,A240,A241;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A243: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A244: pa`1-p`1 = r2 by A238,XCMPLX_1:26;
(pa`1-p`1)^2=(p`1-pa`1)^2 by Lm9;
then A245: (p`1 - pa`1)^2 <= (r/2)^2 by A234,A237,A244,SQUARE_1:77;
A246: pa`2-p`2 = r2 by A238,XCMPLX_1:26;
A247:(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
(pa`2-p`2)^2<=(r/2)^2 by A234,A237,A246,SQUARE_1:77;
then A248:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A245,A247,REAL_1:55;
A249:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A232,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A232,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A249,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A248,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A243,SQUARE_1:def 4;
then A250:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A230,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A250,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A231,A242,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A251: p`2 = t1 & p`1 = s2;
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
A252:Q is open and A253:p in Q;
consider r be real number such that
A254: r>0 and A255:Ball(q,r) c= Q by A252,A253,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A256:r/2>0 by A254,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A257:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A258: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A259:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A257,AXIOMS:22;
A260: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A261:0<r2 by A256,SQUARE_1:38;
set pa=|[p`1-r2,p`2+r2]|;
A262:pa`1=p`1-r2 & pa`2=p`2+r2 by EUCLID:56;
then A263:pa`2> t1 by A251,A261,REAL_2:174;
A264:pa`1< s2 by A251,A261,A262,REAL_2:174;
(t2-t1)/2<t2-t1 by A260,SEQ_2:4;
then r2<t2-p`2 by A251,A259,AXIOMS:22;
then A265: pa`2<t2 by A262,REAL_1:86;
(s2-s1)/2<s2-s1 by A260,SEQ_2:4;
then r2<p`1-s1 by A251,A259,AXIOMS:22;
then pa`1>s1 by A262,REAL_2:165;
then A266:pa in P1 by A2,A263,A264,A265;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A267: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A268: pa`2-p`2 = r2 by A262,XCMPLX_1:26;
A269:(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
A270:r2^2<= (r/2)^2 by A258,A261,SQUARE_1:77;
p`1-pa`1 =r2 by A262,XCMPLX_1:18;
then A271:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A268,A269,A270,REAL_1:55;
A272:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A256,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A256,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A272,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A271,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A267,SQUARE_1:def 4;
then A273:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A254,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A273,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A255,A266,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
end;
hence x in Cl P1 by A77;
suppose A274: p`1 = s2 & p`2 <= t2 & p`2 >= t1;
now per cases by A274,REAL_1:def 5;
suppose A275: 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
A276:Q is open and A277:p in Q;
consider r being real number such that
A278: r>0 and A279:Ball(q,r) c= Q by A276,A277,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A280:r/2>0 by A278,SEQ_2:3;
A281:r/2<r by A278,SEQ_2:4;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A282:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A283:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A282,AXIOMS:22;
A284:r2<r by A281,A282,AXIOMS:22;
A285: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A286:0<r2 by A280,SQUARE_1:38;
set pa=|[p`1-r2,p`2]|;
A287:pa`2=p`2 & pa`1=p`1-r2 by EUCLID:56;
(s2-s1)/2<s2-s1 by A285,SEQ_2:4;
then r2<p`1-s1 by A275,A283,AXIOMS:22;
then s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A275,A286,A287,
REAL_2:165,174;
then A288:pa in P1 by A2;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A289: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A290:(p`2 - pa`2)^2 =0 by A287,SQUARE_1:60,XCMPLX_1:14;
p`1-pa`1 =r2 by A287,XCMPLX_1:18;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A284,A286,A290,SQUARE_1:78;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A289,SQUARE_1:def 4;
then A291:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A278,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A291,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A279,A288,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A292: p`1 = s2 & 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
A293:Q is open and A294:p in Q;
consider r being real number such that
A295: r>0 and A296:Ball(q,r) c= Q by A293,A294,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A297:r/2>0 by A295,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A298:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A299: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A300:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A298,AXIOMS:22;
A301: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A302:0<r2 by A297,SQUARE_1:38;
set pa=|[p`1-r2,p`2+r2]|;
A303:pa`2=p`2+r2 & pa`1=p`1-r2 by EUCLID:56;
then A304:pa`2> t1 by A292,A302,REAL_2:174;
A305:pa`1< s2 by A292,A302,A303,REAL_2:174;
(s2-s1)/2<s2-s1 by A301,SEQ_2:4;
then r2<p`1-s1 by A292,A300,AXIOMS:22;
then A306: pa`1>s1 by A303,REAL_2:165;
(t2-t1)/2<t2-t1 by A301,SEQ_2:4;
then r2<t2-p`2 by A292,A300,AXIOMS:22;
then pa`2<t2 by A303,REAL_1:86;
then A307:pa in P1 by A2,A304,A305,A306;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A308: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
p`1-pa`1 = r2 by A303,XCMPLX_1:18;
then A309: (p`1 - pa`1)^2 <= (r/2)^2 by A299,A302,SQUARE_1:77;
A310: pa`2-p`2 = r2 by A303,XCMPLX_1:26;
A311:(pa`2-p`2)^2=(p`2-pa`2)^2 by Lm9;
(pa`2-p`2)^2<=(r/2)^2 by A299,A302,A310,SQUARE_1:77;
then A312:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A309,A311,REAL_1:55;
A313:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A297,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A297,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A313,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A312,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A308,SQUARE_1:def 4;
then A314:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A295,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A314,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A296,A307,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
suppose A315: p`1 = s2 & p`2 = t2;
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
A316:Q is open and A317:p in Q;
consider r being real number such that
A318: r>0 and A319:Ball(q,r) c= Q by A316,A317,Lm10,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
A320:r/2>0 by A318,SEQ_2:3;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A321:r2 <= r/2 & r2<=min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:35;
A322: r2 <= r/2 & ( min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2
& min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2) by SQUARE_1:35;
then A323:r2<= r/2 & r2<=(s2-s1)/2 & r2<=
(t2-t1)/2 by A321,AXIOMS:22;
A324: s2-s1>0 & t2-t1>0 by A1,SQUARE_1:11;
then (s2-s1)/2 >0 & (t2-t1)/2>0 by SEQ_2:3;
then 0<min((s2-s1)/2,(t2-t1)/2) by SQUARE_1:38;
then A325:0<r2 by A320,SQUARE_1:38;
set pa=|[p`1-r2,p`2-r2]|;
A326:pa`1=p`1-r2 & pa`2=p`2-r2 by EUCLID:56;
then A327:pa`1< s2 by A315,A325,REAL_2:174;
A328:pa`2< t2 by A315,A325,A326,REAL_2:174;
(s2-s1)/2<s2-s1 by A324,SEQ_2:4;
then r2<p`1-s1 by A315,A323,AXIOMS:22;
then A329: pa`1>s1 by A326,REAL_2:165;
(t2-t1)/2<t2-t1 by A324,SEQ_2:4;
then r2<p`2-t1 by A315,A323,AXIOMS:22;
then pa`2>t1 by A326,REAL_2:165;
then A330:pa in P1 by A2,A327,A328,A329;
reconsider qa=pa as Point of Euclid 2 by TOPREAL3:13;
0 <= (p`1 - pa`1)^2 & 0 <= (p`2 - pa`2)^2 by SQUARE_1:72;
then A331: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by REAL_1:55;
A332: p`1-pa`1 = r2 by A326,XCMPLX_1:18;
A333:r2^2<= (r/2)^2 by A322,A325,SQUARE_1:77;
p`2-pa`2 =r2 by A326,XCMPLX_1:18;
then A334:(p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r/2)^2
by A332,A333,REAL_1:55;
A335:r^2=(r/2+r/2)^2 by XCMPLX_1:66
.=(r/2)^2+2*(r/2)*(r/2)+(r/2)^2 by SQUARE_1:63
.=(r/2)^2+(r/2)^2+2*(r/2)*(r/2) by XCMPLX_1:1;
2*(r/2)>0 by A320,REAL_2:122;
then 2*(r/2)*(r/2)>0 by A320,REAL_2:122;
then r^2>(r/2)^2+(r/2)^2 by A335,REAL_2:174;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A334,AXIOMS:22;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A331,SQUARE_1:def 4;
then A336:sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r
by A318,SQUARE_1:77;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A336,TOPREAL3:12;
then pa in Ball(q,r) by METRIC_1:12;
hence thesis by A319,A330,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 13;
end;
hence x in Cl P1 by A77;
end;
hence x in Cl P1;
end;
then P c= Cl P1 /\ P1` by A68,XBOOLE_1:19;
hence thesis by SUBSET_1:32;
end;
hence thesis by A14,A15,A76,XBOOLE_0:def 10;
end;
theorem Th43:
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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
P1 c= [#] ((TOP-REAL 2)|P`)
proof let s1,s2,t1,t2,P,P1;
assume that
A1: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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2};
let x be set;assume A2: x in P1;
then A3: ex pa being Point of TOP-REAL 2 st pa=x &
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A1;
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 A3;
end;
then x in P` by A1,A2,SUBSET_1:50;
hence thesis by PRE_TOPC:def 10;
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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
P1 is Subset of (TOP-REAL 2)|P`
proof let s1,s2,t1,t2,P,P1;assume that
A1: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<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2};
P1 c= [#]((TOP-REAL 2)|P`)by A1,Th43;
hence thesis by PRE_TOPC:16;
end;
theorem Th45:
for s1,s2,t1,t2,P,P2 st s1<s2 & t1<t2 &
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} &
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<s2 & t1<t2 and
A2:
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}
& 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 set;assume A3: x in P2;
then A4: 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 A2;
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,A4;
end;
then x in P` by A2,A3,SUBSET_1:50;
hence thesis by PRE_TOPC:def 10;
end;
theorem
for s1,s2,t1,t2,P,P2 st s1<s2 & t1< t2 &
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} &
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<s2 & t1<t2 and
A2: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}
& 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,Th45;
hence thesis by PRE_TOPC:16;
end;
begin
::
:: The Jordan's property
::
definition let S be Subset of TOP-REAL 2;
attr S is Jordan means :Def2:
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_of (TOP-REAL 2)|S` &
C2 is_a_component_of (TOP-REAL 2)|S`;
synonym S has_property_J;
end;
theorem
for S being Subset of TOP-REAL 2 st S has_property_J 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_of (TOP-REAL 2)|S` &
C2 is_a_component_of (TOP-REAL 2)|S` &
for C3 being Subset of (TOP-REAL 2)|S` st
C3 is_a_component_of (TOP-REAL 2)|S` holds C3 = C1 or C3 = C2
proof
let S be Subset of TOP-REAL 2;
assume A1: S has_property_J;
then reconsider S' = S` as non empty Subset of TOP-REAL 2
by Def2;
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_of (TOP-REAL 2)|S`
& C2 is_a_component_of (TOP-REAL 2)|S`) by A1,Def2;
A6:A1 c= S` & A2 c= S` by A2,XBOOLE_1:7;
A7:[#]((TOP-REAL 2)|S`)=S` by PRE_TOPC:def 10;
A1 c= [#]((TOP-REAL 2)|S`) & A2 c= [#]
((TOP-REAL 2)|S`) by A6,PRE_TOPC:def 10;
then reconsider G0A=A1,G0B=A2 as Subset of (TOP-REAL 2)|S'
by PRE_TOPC:16;
G0A=A1 & G0B=A2;
then A8:G0A is_a_component_of (TOP-REAL 2)|S'
& G0B is_a_component_of (TOP-REAL 2)|S' by A5;
now let C3 be Subset of (TOP-REAL 2)|S';
assume A9: C3 is_a_component_of (TOP-REAL 2)|S';
then A10: C3 <>{}((TOP-REAL 2)|S') by CONNSP_1:34;
C3 /\(G0A \/ G0B)=C3 by A2,A7,PRE_TOPC:15;
then A11: (C3 /\ G0A) \/ (C3 /\ G0B) <>{} by A10,XBOOLE_1:23;
now per cases by A11;
suppose C3 /\ G0A<>{};
then C3 meets G0A by XBOOLE_0:def 7;
then A12:not (C3,G0A are_separated) by CONNSP_1:2;
A13:C3 is connected & G0A is connected by A8,A9,CONNSP_1:def 5;
then A14:C3 \/ G0A is connected by A12,CONNSP_1:18;
G0A c= C3 \/ G0A by XBOOLE_1:7;
then G0A=C3 \/ G0A by A8,A14,CONNSP_1:def 5;
then C3 c= G0A by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A9,A13,CONNSP_1:def 5;
suppose C3 /\ A2<>{};
then C3 meets G0B by XBOOLE_0:def 7;
then A15:not (C3,G0B are_separated) by CONNSP_1:2;
A16:C3 is connected & G0B is connected by A8,A9,CONNSP_1:def 5;
then A17:C3 \/ G0B is connected by A15,CONNSP_1:18;
G0B c= C3 \/ G0B by XBOOLE_1:7;
then G0B=C3 \/ G0B by A8,A17,CONNSP_1:def 5;
then C3 c= G0B by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A9,A16,CONNSP_1:def 5;
end;
hence C3=G0A or C3=G0B;
end;
hence thesis by A2,A3,A4,A8;
end;
theorem
for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
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}
holds P has_property_J
proof let s1,s2,t1,t2; let P be Subset of TOP-REAL 2;assume that
A1: s1<s2 & t1<t2 and
A2: 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};
{pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2}
is Subset of TOP-REAL 2 &
{pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)}
is Subset of TOP-REAL 2 by Th34,Th35;
then reconsider P1= {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2},
P2= {pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)}
as Subset of TOP-REAL 2;
reconsider PC = P` as Subset of TOP-REAL 2;
A3:P1= {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2}&
P2= {pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)};
then A4:PC=P1 \/ P2 & PC<>{} & P1 misses P2 by A1,A2,Th41;
A5:P=(Cl P1)\P1 & P=(Cl P2)\P2 by A1,A2,A3,Th42;
for P1A,P2B be Subset of (TOP-REAL 2)|P`
holds P1A=P1 & P2B=P2 implies
P1A is_a_component_of (TOP-REAL 2)|P`
& P2B is_a_component_of (TOP-REAL 2)|P` by A1,A2,Th41;
hence thesis by A4,A5,Def2;
end;