:: JORDAN6 semantic presentation
begin
theorem Th1: :: JORDAN6:1
for r, s being real number st r <= s holds
( r <= (r + s) / 2 & (r + s) / 2 <= s )
proof
let r, s be real number ; ::_thesis: ( r <= s implies ( r <= (r + s) / 2 & (r + s) / 2 <= s ) )
assume A1: r <= s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )
percases ( r < s or r = s ) by A1, XXREAL_0:1;
suppose r < s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )
hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) by XREAL_1:226; ::_thesis: verum
end;
suppose r = s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )
hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) ; ::_thesis: verum
end;
end;
end;
theorem Th2: :: JORDAN6:2
for TX being non empty TopSpace
for P being Subset of TX
for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
proof
let TX be non empty TopSpace; ::_thesis: for P being Subset of TX
for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let P be Subset of TX; ::_thesis: for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let A be Subset of (TX | P); ::_thesis: for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let B be Subset of TX; ::_thesis: ( B is closed & A = B /\ P implies A is closed )
assume that
A1: B is closed and
A2: A = B /\ P ; ::_thesis: A is closed
[#] (TX | P) = P by PRE_TOPC:def_5;
hence A is closed by A1, A2, PRE_TOPC:13; ::_thesis: verum
end;
theorem Th3: :: JORDAN6:3
for TX, TY being non empty TopSpace
for P being non empty Subset of TY
for f being Function of TX,(TY | P) holds
( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous ) )
proof
let TX, TY be non empty TopSpace; ::_thesis: for P being non empty Subset of TY
for f being Function of TX,(TY | P) holds
( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous ) )
let P be non empty Subset of TY; ::_thesis: for f being Function of TX,(TY | P) holds
( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous ) )
let f be Function of TX,(TY | P); ::_thesis: ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous ) )
A1: the carrier of (TY | P) = [#] (TY | P)
.= P by PRE_TOPC:def_5 ;
hence f is Function of TX,TY by FUNCT_2:7; ::_thesis: for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous
let f2 be Function of TX,TY; ::_thesis: ( f2 = f & f is continuous implies f2 is continuous )
assume that
A2: f2 = f and
A3: f is continuous ; ::_thesis: f2 is continuous
let P1 be Subset of TY; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f2 " P1 is closed )
assume A4: P1 is closed ; ::_thesis: f2 " P1 is closed
reconsider P3 = P1 /\ P as Subset of (TY | P) by TOPS_2:29;
A5: P3 is closed by A4, Th2;
f2 " P = the carrier of TX by A1, A2, FUNCT_2:40
.= dom f2 by FUNCT_2:def_1 ;
then f2 " P1 = (f2 " P1) /\ (f2 " P) by RELAT_1:132, XBOOLE_1:28
.= f " P3 by A2, FUNCT_1:68 ;
hence f2 " P1 is closed by A3, A5, PRE_TOPC:def_6; ::_thesis: verum
end;
theorem Th4: :: JORDAN6:4
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } ; ::_thesis: P is closed
A2: 1 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `1 < r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `1 < r } )
assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `1 < r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4;
then A5: not x in P by XBOOLE_0:def_5;
reconsider q = x as Point of (TOP-REAL 2) by A4;
q `1 < r by A1, A5;
hence x in { p where p is Point of (TOP-REAL 2) : p `1 < r } ; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : p `1 < r } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 < r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `1 < r } ; ::_thesis: x in P `
then A6: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 < r ) ;
now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`1_>=_r__}_
assume x in { q where q is Point of (TOP-REAL 2) : q `1 >= r } ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = x & q `1 >= r ) ;
hence contradiction by A6; ::_thesis: verum
end;
then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5;
hence x in P ` by SUBSET_1:def_4; ::_thesis: verum
end;
then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `1 < r } by A3, XBOOLE_0:def_10;
A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 1 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } )
assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 }
then consider p being Point of (TOP-REAL 2) such that
A9: p = x and
A10: p `1 < r by A7;
p /. 1 < r by A10, JORDAN2B:29;
hence x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } by A9; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : r > p /. 1 } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } ; ::_thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A11: q = x and
A12: r > q /. 1 ;
q `1 < r by A12, JORDAN2B:29;
hence x in P ` by A7, A11; ::_thesis: verum
end;
then A13: P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 1 } by A8, XBOOLE_0:def_10;
reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A13, JORDAN2B:12;
hence P is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th5: :: JORDAN6:5
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } ; ::_thesis: P is closed
A2: 1 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `1 > r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `1 > r } )
assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `1 > r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4;
then A5: not x in P by XBOOLE_0:def_5;
reconsider q = x as Point of (TOP-REAL 2) by A4;
q `1 > r by A1, A5;
hence x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : p `1 > r } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 > r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; ::_thesis: x in P `
then A6: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 > r ) ;
now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`1_<=_r__}_
assume x in { q where q is Point of (TOP-REAL 2) : q `1 <= r } ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = x & q `1 <= r ) ;
hence contradiction by A6; ::_thesis: verum
end;
then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5;
hence x in P ` by SUBSET_1:def_4; ::_thesis: verum
end;
then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `1 > r } by A3, XBOOLE_0:def_10;
A8: P ` c= { p where p is Point of (TOP-REAL 2) : r < p /. 1 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } )
assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 }
then consider p being Point of (TOP-REAL 2) such that
A9: p = x and
A10: p `1 > r by A7;
p /. 1 > r by A10, JORDAN2B:29;
hence x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } by A9; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : r < p /. 1 } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } ; ::_thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A11: q = x and
A12: r < q /. 1 ;
q `1 > r by A12, JORDAN2B:29;
hence x in P ` by A7, A11; ::_thesis: verum
end;
then A13: P ` = { p where p is Point of (TOP-REAL 2) : r < p /. 1 } by A8, XBOOLE_0:def_10;
reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A13, JORDAN2B:13;
hence P is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th6: :: JORDAN6:6
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 = r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 = r } ; ::_thesis: P is closed
defpred S1[ Point of (TOP-REAL 2)] means $1 `1 >= r;
{ p where p is Element of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `1 >= r } as Subset of (TOP-REAL 2) ;
A2: P1 is closed by Th4;
defpred S2[ Point of (TOP-REAL 2)] means $1 `1 <= r;
{ p where p is Element of (TOP-REAL 2) : S2[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `1 <= r } as Subset of (TOP-REAL 2) ;
A3: P2 is closed by Th5;
A4: P c= P1 /\ P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 )
assume x in P ; ::_thesis: x in P1 /\ P2
then A5: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = r ) by A1;
then A6: x in P1 ;
x in P2 by A5;
hence x in P1 /\ P2 by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
P1 /\ P2 c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P )
assume A7: x in P1 /\ P2 ; ::_thesis: x in P
then A8: x in P1 by XBOOLE_0:def_4;
A9: x in P2 by A7, XBOOLE_0:def_4;
consider q1 being Point of (TOP-REAL 2) such that
A10: q1 = x and
A11: q1 `1 >= r by A8;
ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 <= r ) by A9;
then q1 `1 = r by A10, A11, XXREAL_0:1;
hence x in P by A1, A10; ::_thesis: verum
end;
then P = P1 /\ P2 by A4, XBOOLE_0:def_10;
hence P is closed by A2, A3, TOPS_1:8; ::_thesis: verum
end;
theorem Th7: :: JORDAN6:7
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } ; ::_thesis: P is closed
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `2 < r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `2 < r } )
assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `2 < r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4;
then A5: not x in P by XBOOLE_0:def_5;
reconsider q = x as Point of (TOP-REAL 2) by A4;
q `2 < r by A1, A5;
hence x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : p `2 < r } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 < r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; ::_thesis: x in P `
then A6: ex p being Point of (TOP-REAL 2) st
( p = x & p `2 < r ) ;
now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`2_>=_r__}_
assume x in { q where q is Point of (TOP-REAL 2) : q `2 >= r } ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = x & q `2 >= r ) ;
hence contradiction by A6; ::_thesis: verum
end;
then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5;
hence x in P ` by SUBSET_1:def_4; ::_thesis: verum
end;
then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `2 < r } by A3, XBOOLE_0:def_10;
A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 2 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } )
assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 }
then consider p being Point of (TOP-REAL 2) such that
A9: p = x and
A10: p `2 < r by A7;
p /. 2 < r by A10, JORDAN2B:29;
hence x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A9; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : r > p /. 2 } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } ; ::_thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A11: q = x and
A12: r > q /. 2 ;
q `2 < r by A12, JORDAN2B:29;
hence x in P ` by A7, A11; ::_thesis: verum
end;
then A13: P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A8, XBOOLE_0:def_10;
reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A13, JORDAN2B:12;
hence P is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th8: :: JORDAN6:8
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } ; ::_thesis: P is closed
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `2 > r }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `2 > r } )
assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `2 > r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4;
then A5: not x in P by XBOOLE_0:def_5;
reconsider q = x as Point of (TOP-REAL 2) by A4;
q `2 > r by A1, A5;
hence x in { p where p is Point of (TOP-REAL 2) : p `2 > r } ; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : p `2 > r } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 > r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `2 > r } ; ::_thesis: x in P `
then A6: ex p being Point of (TOP-REAL 2) st
( p = x & p `2 > r ) ;
now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`2_<=_r__}_
assume x in { q where q is Point of (TOP-REAL 2) : q `2 <= r } ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = x & q `2 <= r ) ;
hence contradiction by A6; ::_thesis: verum
end;
then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5;
hence x in P ` by SUBSET_1:def_4; ::_thesis: verum
end;
then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `2 > r } by A3, XBOOLE_0:def_10;
A8: P ` c= { p where p is Point of (TOP-REAL 2) : r < p /. 2 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } )
assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 }
then consider p being Point of (TOP-REAL 2) such that
A9: p = x and
A10: p `2 > r by A7;
p /. 2 > r by A10, JORDAN2B:29;
hence x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } by A9; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : r < p /. 2 } c= P `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } ; ::_thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A11: q = x and
A12: r < q /. 2 ;
q `2 > r by A12, JORDAN2B:29;
hence x in P ` by A7, A11; ::_thesis: verum
end;
then A13: P ` = { p where p is Point of (TOP-REAL 2) : r < p /. 2 } by A8, XBOOLE_0:def_10;
reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A13, JORDAN2B:13;
hence P is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th9: :: JORDAN6:9
for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds
P is closed
proof
let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds
P is closed
let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 = r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 = r } ; ::_thesis: P is closed
defpred S1[ Point of (TOP-REAL 2)] means $1 `2 >= r;
{ p where p is Element of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `2 >= r } as Subset of (TOP-REAL 2) ;
A2: P1 is closed by Th7;
defpred S2[ Point of (TOP-REAL 2)] means $1 `2 <= r;
{ p where p is Element of (TOP-REAL 2) : S2[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7();
then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `2 <= r } as Subset of (TOP-REAL 2) ;
A3: P2 is closed by Th8;
A4: P c= P1 /\ P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 )
assume x in P ; ::_thesis: x in P1 /\ P2
then A5: ex p being Point of (TOP-REAL 2) st
( p = x & p `2 = r ) by A1;
then A6: x in P1 ;
x in P2 by A5;
hence x in P1 /\ P2 by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
P1 /\ P2 c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P )
assume A7: x in P1 /\ P2 ; ::_thesis: x in P
then A8: x in P1 by XBOOLE_0:def_4;
A9: x in P2 by A7, XBOOLE_0:def_4;
consider q1 being Point of (TOP-REAL 2) such that
A10: q1 = x and
A11: q1 `2 >= r by A8;
ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 <= r ) by A9;
then q1 `2 = r by A10, A11, XXREAL_0:1;
hence x in P by A1, A10; ::_thesis: verum
end;
then P = P1 /\ P2 by A4, XBOOLE_0:def_10;
hence P is closed by A2, A3, TOPS_1:8; ::_thesis: verum
end;
theorem Th10: :: JORDAN6:10
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is connected
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is connected
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is connected
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies P is connected )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: P is connected
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A2: f is being_homeomorphism and
f . 0 = p1 and
f . 1 = p2 by TOPREAL1:def_1;
reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
A3: f is continuous Function of I[01],((TOP-REAL n) | P9) by A2, TOPS_2:def_5;
A4: [#] I[01] is connected by CONNSP_1:27, TREAL_1:19;
A5: rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def_5;
A6: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5;
dom f = [#] I[01] by A2, TOPS_2:def_5;
then A7: P = f .: ([#] I[01]) by A5, A6, RELAT_1:113;
f .: ([#] I[01]) is connected by A3, A4, TOPS_2:61;
hence P is connected by A7, CONNSP_1:23; ::_thesis: verum
end;
theorem :: JORDAN6:11
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
P is closed by COMPTS_1:7, JORDAN5A:1;
theorem Th12: :: JORDAN6:12
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )
then A2: p1 in P by TOPREAL1:1;
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL 2) | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by A1, TOPREAL1:def_1;
A6: f is continuous by A3, TOPS_2:def_5;
consider h being Function of (TOP-REAL 2),R^1 such that
A7: for p being Element of (TOP-REAL 2) holds h . p = p /. 1 by JORDAN2B:1;
1 in Seg 2 by FINSEQ_1:1;
then A8: h is continuous by A7, JORDAN2B:18;
A9: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P9 by PRE_TOPC:def_5 ;
then A10: f is Function of the carrier of I[01], the carrier of (TOP-REAL 2) by FUNCT_2:7;
reconsider f1 = f as Function of I[01],(TOP-REAL 2) by A9, FUNCT_2:7;
A11: f1 is continuous by A6, Th3;
reconsider g = h * f as Function of I[01],R^1 by A10;
A12: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1;
then A13: 0 in dom f by XXREAL_1:1;
A14: 1 in dom f by A12, XXREAL_1:1;
A15: g . 0 = h . (f . 0) by A13, FUNCT_1:13
.= p1 /. 1 by A4, A7
.= p1 `1 by JORDAN2B:29 ;
A16: g . 1 = h . (f . 1) by A14, FUNCT_1:13
.= p2 /. 1 by A5, A7
.= p2 `1 by JORDAN2B:29 ;
percases ( g . 0 <> g . 1 or g . 0 = g . 1 ) ;
suppose g . 0 <> g . 1 ; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )
then consider r1 being Real such that
A17: 0 < r1 and
A18: r1 < 1 and
A19: g . r1 = ((p1 `1) + (p2 `1)) / 2 by A8, A11, A15, A16, TOPREAL5:9;
A20: r1 in [.0,1.] by A17, A18, XXREAL_1:1;
A21: r1 in the carrier of I[01] by A17, A18, BORSUK_1:40, XXREAL_1:1;
then reconsider q1 = f . r1 as Point of (TOP-REAL 2) by A10, FUNCT_2:5;
g . r1 = h . (f . r1) by A12, A20, FUNCT_1:13
.= q1 /. 1 by A7
.= q1 `1 by JORDAN2B:29 ;
hence ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by A9, A19, A21, FUNCT_2:5; ::_thesis: verum
end;
suppose g . 0 = g . 1 ; ::_thesis: ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )
hence ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by A2, A15, A16; ::_thesis: verum
end;
end;
end;
theorem Th13: :: JORDAN6:13
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
( P meets Q & P /\ Q is closed )
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
( P meets Q & P /\ Q is closed )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies ( P meets Q & P /\ Q is closed ) )
reconsider W = P as Subset of (TOP-REAL 2) ;
assume A1: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ) ; ::_thesis: ( P meets Q & P /\ Q is closed )
consider f being Function of (TOP-REAL 2),R^1 such that
A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 1 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
A3: 1 in Seg 2 by FINSEQ_1:1;
A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ;
A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61
.= P by XBOOLE_1:28 ;
rng (f | P) c= the carrier of R^1 ;
then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def_1, RELSET_1:4;
reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7;
A8: p1 in P by A1, TOPREAL1:1;
A9: p2 in P by A1, TOPREAL1:1;
reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1;
A10: g . p19 = f . p1 by A8, FUNCT_1:49
.= p1 /. 1 by A2
.= p1 `1 by JORDAN2B:29 ;
A11: g . p29 = f . p2 by A9, FUNCT_1:49
.= p2 /. 1 by A2
.= p2 `1 by JORDAN2B:29 ;
W is connected by A1, Th10;
then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def_3;
A13: now__::_thesis:_(_(_p1_`1_<=_p2_`1_&_P_meets_Q_)_or_(_p1_`1_>_p2_`1_&_P_meets_Q_)_)
percases ( p1 `1 <= p2 `1 or p1 `1 > p2 `1 ) ;
caseA14: p1 `1 <= p2 `1 ; ::_thesis: P meets Q
then A15: p1 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1;
((p1 `1) + (p2 `1)) / 2 <= p2 `1 by A14, Th1;
then consider xc being Point of ((TOP-REAL 2) | P) such that
A16: g . xc = ((p1 `1) + (p2 `1)) / 2 by A10, A11, A12, A15, TOPREAL5:4;
xc in P by A6;
then reconsider pc = xc as Point of (TOP-REAL 2) ;
g . xc = f . xc by A5, FUNCT_1:49
.= pc /. 1 by A2
.= pc `1 by JORDAN2B:29 ;
then xc in Q by A1, A16;
hence P meets Q by A6, XBOOLE_0:3; ::_thesis: verum
end;
caseA17: p1 `1 > p2 `1 ; ::_thesis: P meets Q
then A18: p2 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1;
((p1 `1) + (p2 `1)) / 2 <= p1 `1 by A17, Th1;
then consider xc being Point of ((TOP-REAL 2) | P) such that
A19: g . xc = ((p1 `1) + (p2 `1)) / 2 by A10, A11, A12, A18, TOPREAL5:4;
xc in P by A6;
then reconsider pc = xc as Point of (TOP-REAL 2) ;
g . xc = f . xc by A5, FUNCT_1:49
.= pc /. 1 by A2
.= pc `1 by JORDAN2B:29 ;
then xc in Q by A1, A19;
hence P meets Q by A6, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
reconsider P1 = P, Q1 = Q as Subset of (TOP-REAL 2) ;
A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1;
Q1 is closed by A1, Th6;
hence ( P meets Q & P /\ Q is closed ) by A13, A20, TOPS_1:8; ::_thesis: verum
end;
theorem Th14: :: JORDAN6:14
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
( P meets Q & P /\ Q is closed )
proof
let P, Q1 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
( P meets Q1 & P /\ Q1 is closed )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies ( P meets Q1 & P /\ Q1 is closed ) )
assume A1: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ) ; ::_thesis: ( P meets Q1 & P /\ Q1 is closed )
consider f being Function of (TOP-REAL 2),R^1 such that
A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 2 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
A3: 2 in Seg 2 by FINSEQ_1:1;
A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ;
A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61
.= P by XBOOLE_1:28 ;
rng (f | P) c= the carrier of R^1 ;
then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def_1, RELSET_1:4;
reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7;
A8: p1 in P by A1, TOPREAL1:1;
A9: p2 in P by A1, TOPREAL1:1;
reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1;
A10: g . p19 = f . p1 by A8, FUNCT_1:49
.= p1 /. 2 by A2
.= p1 `2 by JORDAN2B:29 ;
A11: g . p29 = f . p2 by A9, FUNCT_1:49
.= p2 /. 2 by A2
.= p2 `2 by JORDAN2B:29 ;
reconsider W = P as Subset of (TOP-REAL 2) ;
W is connected by A1, Th10;
then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def_3;
A13: now__::_thesis:_(_(_p1_`2_<=_p2_`2_&_P_meets_Q1_)_or_(_p1_`2_>_p2_`2_&_P_meets_Q1_)_)
percases ( p1 `2 <= p2 `2 or p1 `2 > p2 `2 ) ;
caseA14: p1 `2 <= p2 `2 ; ::_thesis: P meets Q1
then A15: p1 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1;
((p1 `2) + (p2 `2)) / 2 <= p2 `2 by A14, Th1;
then consider xc being Point of ((TOP-REAL 2) | P) such that
A16: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A15, TOPREAL5:4;
xc in P by A6;
then reconsider pc = xc as Point of (TOP-REAL 2) ;
g . xc = f . xc by A5, FUNCT_1:49
.= pc /. 2 by A2
.= pc `2 by JORDAN2B:29 ;
then xc in Q1 by A1, A16;
hence P meets Q1 by A6, XBOOLE_0:3; ::_thesis: verum
end;
caseA17: p1 `2 > p2 `2 ; ::_thesis: P meets Q1
then A18: p2 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1;
((p1 `2) + (p2 `2)) / 2 <= p1 `2 by A17, Th1;
then consider xc being Point of ((TOP-REAL 2) | P) such that
A19: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A18, TOPREAL5:4;
xc in P by A6;
then reconsider pc = xc as Point of (TOP-REAL 2) ;
g . xc = f . xc by A5, FUNCT_1:49
.= pc /. 2 by A2
.= pc `2 by JORDAN2B:29 ;
then xc in Q1 by A1, A19;
hence P meets Q1 by A6, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
reconsider P1 = P, Q2 = Q1 as Subset of (TOP-REAL 2) ;
A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1;
Q2 is closed by A1, Th9;
hence ( P meets Q1 & P /\ Q1 is closed ) by A13, A20, TOPS_1:8; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
func x_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN6:def 1
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
it = First_Point (P,p1,p2,Q);
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b1 = First_Point (P,p1,p2,Q)
proof
{ q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider Q1 = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } as Subset of (TOP-REAL 2) ;
reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ;
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q2 = First_Point (P,p1,p2,Q) ;
hence ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
proof
let q3, q4 be Point of (TOP-REAL 2); ::_thesis: ( ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q3 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 )
assume A1: ( ( for Q1 being Subset of (TOP-REAL 2) st Q1 = { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } holds
q4 = First_Point (P,p1,p2,Q2) ) ) ; ::_thesis: q3 = q4
{ q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } as Subset of (TOP-REAL 2) ;
q3 = First_Point (P,p1,p2,Q3) by A1;
hence q3 = q4 by A1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines x_Middle JORDAN6:def_1_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, b4 being Point of (TOP-REAL 2) holds
( b4 = x_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b4 = First_Point (P,p1,p2,Q) );
definition
let P be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
func y_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN6:def 2
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
it = First_Point (P,p1,p2,Q);
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b1 = First_Point (P,p1,p2,Q)
proof
{ q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } as Subset of (TOP-REAL 2) ;
reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ;
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
q2 = First_Point (P,p1,p2,Q) ;
hence ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
proof
let q3, q4 be Point of (TOP-REAL 2); ::_thesis: ( ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
q3 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 )
assume A1: ( ( for Q1 being Subset of (TOP-REAL 2) st Q1 = { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } holds
q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } holds
q4 = First_Point (P,p1,p2,Q2) ) ) ; ::_thesis: q3 = q4
{ q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } as Subset of (TOP-REAL 2) ;
q3 = First_Point (P,p1,p2,Q3) by A1;
hence q3 = q4 by A1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines y_Middle JORDAN6:def_2_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, b4 being Point of (TOP-REAL 2) holds
( b4 = y_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b4 = First_Point (P,p1,p2,Q) );
theorem :: JORDAN6:15
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P )
deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;
defpred S1[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2;
reconsider Q = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8();
A2: x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q) by Def1;
A3: P meets Q by A1, Th13;
P /\ Q is closed by A1, Th13;
then A4: x_Middle (P,p1,p2) in P /\ Q by A1, A2, A3, JORDAN5C:def_1;
defpred S2[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2) + (p2 `2)) / 2;
reconsider Q2 = { H1(q) where q is Point of (TOP-REAL 2) : S2[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8();
A5: y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q2) by Def2;
A6: P meets Q2 by A1, Th14;
P /\ Q2 is closed by A1, Th14;
then y_Middle (P,p1,p2) in P /\ Q2 by A1, A5, A6, JORDAN5C:def_1;
hence ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: JORDAN6:16
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )
A2: now__::_thesis:_(_p1_=_x_Middle_(P,p1,p2)_implies_p1_`1_=_p2_`1_)
assume A3: p1 = x_Middle (P,p1,p2) ; ::_thesis: p1 `1 = p2 `1
deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;
defpred S1[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2;
reconsider Q1 = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8();
A4: P meets Q1 by A1, Th13;
A5: P /\ Q1 is closed by A1, Th13;
x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def1;
then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def_1;
then p1 in Q1 by XBOOLE_0:def_4;
then ex q being Point of (TOP-REAL 2) st
( q = p1 & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ;
hence p1 `1 = p2 `1 ; ::_thesis: verum
end;
now__::_thesis:_(_p1_`1_=_p2_`1_implies_p1_=_x_Middle_(P,p1,p2)_)
assume A6: p1 `1 = p2 `1 ; ::_thesis: p1 = x_Middle (P,p1,p2)
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
p1 = First_Point (P,p1,p2,Q)
proof
let Q be Subset of (TOP-REAL 2); ::_thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )
assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: p1 = First_Point (P,p1,p2,Q)
then A8: p1 in Q by A6;
P /\ Q is closed by A1, A7, Th13;
hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; ::_thesis: verum
end;
hence p1 = x_Middle (P,p1,p2) by Def1; ::_thesis: verum
end;
hence ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) by A2; ::_thesis: verum
end;
theorem :: JORDAN6:17
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
A2: now__::_thesis:_(_p1_=_y_Middle_(P,p1,p2)_implies_p1_`2_=_p2_`2_)
assume A3: p1 = y_Middle (P,p1,p2) ; ::_thesis: p1 `2 = p2 `2
deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;
defpred S1[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2) + (p2 `2)) / 2;
reconsider Q1 = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8();
A4: P meets Q1 by A1, Th14;
A5: P /\ Q1 is closed by A1, Th14;
y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def2;
then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def_1;
then p1 in Q1 by XBOOLE_0:def_4;
then ex q being Point of (TOP-REAL 2) st
( q = p1 & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;
hence p1 `2 = p2 `2 ; ::_thesis: verum
end;
now__::_thesis:_(_p1_`2_=_p2_`2_implies_p1_=_y_Middle_(P,p1,p2)_)
assume A6: p1 `2 = p2 `2 ; ::_thesis: p1 = y_Middle (P,p1,p2)
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
p1 = First_Point (P,p1,p2,Q)
proof
let Q be Subset of (TOP-REAL 2); ::_thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )
assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: p1 = First_Point (P,p1,p2,Q)
then A8: p1 in Q by A6;
P /\ Q is closed by A1, A7, Th14;
hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; ::_thesis: verum
end;
hence p1 = y_Middle (P,p1,p2) by Def2; ::_thesis: verum
end;
hence ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) by A2; ::_thesis: verum
end;
begin
theorem Th18: :: JORDAN6:18
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 holds
LE q2,q1,P,p2,p1
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 holds
LE q2,q1,P,p2,p1
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 implies LE q2,q1,P,p2,p1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 ; ::_thesis: LE q2,q1,P,p2,p1
thus ( q2 in P & q1 in P ) by A2, JORDAN5C:def_3; :: according to JORDAN5C:def_3 ::_thesis: for b1 being Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
for b2, b3 being Element of REAL holds
( not b1 is being_homeomorphism or not b1 . 0 = p2 or not b1 . 1 = p1 or not b1 . b2 = q2 or not 0 <= b2 or not b2 <= 1 or not b1 . b3 = q1 or not 0 <= b3 or not b3 <= 1 or b2 <= b3 )
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for b1, b2 being Element of REAL holds
( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b1 = q2 or not 0 <= b1 or not b1 <= 1 or not f . b2 = q1 or not 0 <= b2 or not b2 <= 1 or b1 <= b2 )
let s1, s2 be Real; ::_thesis: ( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . s1 = q2 or not 0 <= s1 or not s1 <= 1 or not f . s2 = q1 or not 0 <= s2 or not s2 <= 1 or s1 <= s2 )
assume that
A3: f is being_homeomorphism and
A4: f . 0 = p2 and
A5: f . 1 = p1 and
A6: f . s1 = q2 and
A7: 0 <= s1 and
A8: s1 <= 1 and
A9: f . s2 = q1 and
A10: 0 <= s2 and
A11: s2 <= 1 ; ::_thesis: s1 <= s2
A12: 1 - 0 >= 1 - s1 by A7, XREAL_1:13;
A13: 1 - 0 >= 1 - s2 by A10, XREAL_1:13;
A14: 1 - 1 <= 1 - s1 by A8, XREAL_1:13;
A15: 1 - 1 <= 1 - s2 by A11, XREAL_1:13;
set Ex = L[01] (((0,1) (#)),((#) (0,1)));
A16: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;
set g = f * (L[01] (((0,1) (#)),((#) (0,1))));
A17: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9;
A18: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9;
dom f = [#] I[01] by A3, TOPS_2:def_5;
then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A16, TOPMETR:20, TOPS_2:def_5;
then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;
then A19: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A16, TOPMETR:20, TOPS_2:def_5;
reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P9) by TOPMETR:20;
A20: g is being_homeomorphism by A3, A16, TOPMETR:20, TOPS_2:57;
A21: 1 - s1 in dom g by A12, A14, A19, BORSUK_1:43;
A22: 1 - s2 in dom g by A13, A15, A19, BORSUK_1:43;
A23: g . 0 = p1 by A5, A18, A19, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5;
A24: g . 1 = p2 by A4, A17, A19, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5;
reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of (Closed-Interval-TSpace (0,1)) by A12, A13, A14, A15, BORSUK_1:43, TOPMETR:20;
A25: (L[01] (((0,1) (#)),((#) (0,1)))) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= s1 ;
A26: (L[01] (((0,1) (#)),((#) (0,1)))) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= s2 ;
A27: g . (1 - s1) = q2 by A6, A21, A25, FUNCT_1:12;
g . (1 - s2) = q1 by A9, A22, A26, FUNCT_1:12;
then 1 - s2 <= 1 - s1 by A2, A12, A13, A14, A20, A23, A24, A27, JORDAN5C:def_3;
then s1 <= 1 - (1 - s2) by XREAL_1:11;
hence s1 <= s2 ; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
let p1, p2, q1 be Point of (TOP-REAL 2);
func L_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 3
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;
coherence
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2)
proof
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & LE q,q1,P,p1,p2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
end;
:: deftheorem defines L_Segment JORDAN6:def_3_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;
definition
let P be Subset of (TOP-REAL 2);
let p1, p2, q1 be Point of (TOP-REAL 2);
func R_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 4
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;
coherence
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2)
proof
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
end;
:: deftheorem defines R_Segment JORDAN6:def_4_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;
theorem Th19: :: JORDAN6:19
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: L_Segment (P,p1,p2,q1) c= P
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,q1) or x in P )
assume x in L_Segment (P,p1,p2,q1) ; ::_thesis: x in P
then ex q being Point of (TOP-REAL 2) st
( q = x & LE q,q1,P,p1,p2 ) ;
hence x in P by JORDAN5C:def_3; ::_thesis: verum
end;
theorem Th20: :: JORDAN6:20
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: R_Segment (P,p1,p2,q1) c= P
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p1,p2,q1) or x in P )
assume x in R_Segment (P,p1,p2,q1) ; ::_thesis: x in P
then ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 ) ;
hence x in P by JORDAN5C:def_3; ::_thesis: verum
end;
theorem :: JORDAN6:21
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,p1) = {p1}
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,p1) = {p1}
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p1) = {p1} )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,p1) = {p1}
then A2: p1 in P by TOPREAL1:1;
thus L_Segment (P,p1,p2,p1) c= {p1} :: according to XBOOLE_0:def_10 ::_thesis: {p1} c= L_Segment (P,p1,p2,p1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,p1) or x in {p1} )
assume x in L_Segment (P,p1,p2,p1) ; ::_thesis: x in {p1}
then consider q being Point of (TOP-REAL 2) such that
A3: q = x and
A4: LE q,p1,P,p1,p2 ;
q in P by A4, JORDAN5C:def_3;
then LE p1,q,P,p1,p2 by A1, JORDAN5C:10;
then q = p1 by A1, A4, JORDAN5C:12;
hence x in {p1} by A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1} or x in L_Segment (P,p1,p2,p1) )
assume x in {p1} ; ::_thesis: x in L_Segment (P,p1,p2,p1)
then A5: x = p1 by TARSKI:def_1;
LE p1,p1,P,p1,p2 by A2, JORDAN5C:9;
hence x in L_Segment (P,p1,p2,p1) by A5; ::_thesis: verum
end;
theorem :: JORDAN6:22
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,p2) = P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,p2) = P
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p2) = P )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,p2) = P
thus L_Segment (P,p1,p2,p2) c= P by Th19; :: according to XBOOLE_0:def_10 ::_thesis: P c= L_Segment (P,p1,p2,p2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in L_Segment (P,p1,p2,p2) )
assume A2: x in P ; ::_thesis: x in L_Segment (P,p1,p2,p2)
then reconsider p = x as Point of (TOP-REAL 2) ;
LE p,p2,P,p1,p2 by A1, A2, JORDAN5C:10;
hence x in L_Segment (P,p1,p2,p2) ; ::_thesis: verum
end;
theorem :: JORDAN6:23
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,p2) = {p2}
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,p2) = {p2}
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,p2) = {p2} )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,p2) = {p2}
then A2: p2 in P by TOPREAL1:1;
thus R_Segment (P,p1,p2,p2) c= {p2} :: according to XBOOLE_0:def_10 ::_thesis: {p2} c= R_Segment (P,p1,p2,p2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p1,p2,p2) or x in {p2} )
assume x in R_Segment (P,p1,p2,p2) ; ::_thesis: x in {p2}
then consider q being Point of (TOP-REAL 2) such that
A3: q = x and
A4: LE p2,q,P,p1,p2 ;
q in P by A4, JORDAN5C:def_3;
then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;
then q = p2 by A1, A4, JORDAN5C:12;
hence x in {p2} by A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p2} or x in R_Segment (P,p1,p2,p2) )
assume x in {p2} ; ::_thesis: x in R_Segment (P,p1,p2,p2)
then A5: x = p2 by TARSKI:def_1;
LE p2,p2,P,p1,p2 by A2, JORDAN5C:9;
hence x in R_Segment (P,p1,p2,p2) by A5; ::_thesis: verum
end;
theorem :: JORDAN6:24
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,p1) = P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,p1) = P
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,p1) = P )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,p1) = P
thus R_Segment (P,p1,p2,p1) c= P by Th20; :: according to XBOOLE_0:def_10 ::_thesis: P c= R_Segment (P,p1,p2,p1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in R_Segment (P,p1,p2,p1) )
assume A2: x in P ; ::_thesis: x in R_Segment (P,p1,p2,p1)
then reconsider p = x as Point of (TOP-REAL 2) ;
LE p1,p,P,p1,p2 by A1, A2, JORDAN5C:10;
hence x in R_Segment (P,p1,p2,p1) ; ::_thesis: verum
end;
theorem :: JORDAN6:25
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
A2: { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } )
assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; ::_thesis: x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }
then consider q being Point of (TOP-REAL 2) such that
A3: q = x and
A4: LE q1,q,P,p1,p2 ;
LE q,q1,P,p2,p1 by A1, A4, Th18;
hence x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } by A3; ::_thesis: verum
end;
{ q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } c= { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } or x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } )
assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p2,p1 } ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
then consider q being Point of (TOP-REAL 2) such that
A5: q = x and
A6: LE q,q1,P,p2,p1 ;
LE q1,q,P,p1,p2 by A1, A6, Th18, JORDAN5B:14;
hence x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } by A5; ::_thesis: verum
end;
hence R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
let p1, p2, q1, q2 be Point of (TOP-REAL 2);
func Segment (P,p1,p2,q1,q2) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 5
(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));
correctness
coherence
(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2);
;
end;
:: deftheorem defines Segment JORDAN6:def_5_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));
theorem :: JORDAN6:26
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
thus Segment (P,p1,p2,q1,q2) c= { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } c= Segment (P,p1,p2,q1,q2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Segment (P,p1,p2,q1,q2) or x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } )
assume A1: x in Segment (P,p1,p2,q1,q2) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
then A2: x in R_Segment (P,p1,p2,q1) by XBOOLE_0:def_4;
A3: x in L_Segment (P,p1,p2,q2) by A1, XBOOLE_0:def_4;
A4: ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 ) by A2;
ex p being Point of (TOP-REAL 2) st
( p = x & LE p,q2,P,p1,p2 ) by A3;
hence x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } or x in Segment (P,p1,p2,q1,q2) )
assume x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } ; ::_thesis: x in Segment (P,p1,p2,q1,q2)
then A5: ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) ;
then A6: x in R_Segment (P,p1,p2,q1) ;
x in L_Segment (P,p1,p2,q2) by A5;
hence x in Segment (P,p1,p2,q1,q2) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: JORDAN6:27
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q2,q1,P,p2,p1 holds
LE q1,q2,P,p1,p2 by Th18, JORDAN5B:14;
theorem Th28: :: JORDAN6:28
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q)
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q)
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q)
thus L_Segment (P,p1,p2,q) c= R_Segment (P,p2,p1,q) :: according to XBOOLE_0:def_10 ::_thesis: R_Segment (P,p2,p1,q) c= L_Segment (P,p1,p2,q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,q) or x in R_Segment (P,p2,p1,q) )
assume x in L_Segment (P,p1,p2,q) ; ::_thesis: x in R_Segment (P,p2,p1,q)
then consider p being Point of (TOP-REAL 2) such that
A2: p = x and
A3: LE p,q,P,p1,p2 ;
LE q,p,P,p2,p1 by A1, A3, Th18;
hence x in R_Segment (P,p2,p1,q) by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p2,p1,q) or x in L_Segment (P,p1,p2,q) )
assume x in R_Segment (P,p2,p1,q) ; ::_thesis: x in L_Segment (P,p1,p2,q)
then consider p being Point of (TOP-REAL 2) such that
A4: p = x and
A5: LE q,p,P,p2,p1 ;
LE p,q,P,p1,p2 by A1, A5, Th18, JORDAN5B:14;
hence x in L_Segment (P,p1,p2,q) by A4; ::_thesis: verum
end;
theorem :: JORDAN6:29
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)
then L_Segment (P,p1,p2,q2) = R_Segment (P,p2,p1,q2) by Th28;
hence Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) by A1, Th28, JORDAN5B:14; ::_thesis: verum
end;
begin
definition
let s be real number ;
func Vertical_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 6
{ p where p is Point of (TOP-REAL 2) : p `1 = s } ;
correctness
coherence
{ p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2);
proof
{ p where p is Point of (TOP-REAL 2) : p `1 = s } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 = s } or x in the carrier of (TOP-REAL 2) )
assume x in { p where p is Point of (TOP-REAL 2) : p `1 = s } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = s ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
func Horizontal_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 7
{ p where p is Point of (TOP-REAL 2) : p `2 = s } ;
correctness
coherence
{ p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2);
proof
{ p where p is Point of (TOP-REAL 2) : p `2 = s } c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 = s } or x in the carrier of (TOP-REAL 2) )
assume x in { p where p is Point of (TOP-REAL 2) : p `2 = s } ; ::_thesis: x in the carrier of (TOP-REAL 2)
then ex p being Point of (TOP-REAL 2) st
( p = x & p `2 = s ) ;
hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2) ; ::_thesis: verum
end;
end;
:: deftheorem defines Vertical_Line JORDAN6:def_6_:_
for s being real number holds Vertical_Line s = { p where p is Point of (TOP-REAL 2) : p `1 = s } ;
:: deftheorem defines Horizontal_Line JORDAN6:def_7_:_
for s being real number holds Horizontal_Line s = { p where p is Point of (TOP-REAL 2) : p `2 = s } ;
theorem :: JORDAN6:30
for r being real number holds
( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th6, Th9;
theorem Th31: :: JORDAN6:31
for r being real number
for p being Point of (TOP-REAL 2) holds
( p in Vertical_Line r iff p `1 = r )
proof
let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) holds
( p in Vertical_Line r iff p `1 = r )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in Vertical_Line r iff p `1 = r )
hereby ::_thesis: ( p `1 = r implies p in Vertical_Line r )
assume p in Vertical_Line r ; ::_thesis: p `1 = r
then ex q being Point of (TOP-REAL 2) st
( q = p & q `1 = r ) ;
hence p `1 = r ; ::_thesis: verum
end;
assume p `1 = r ; ::_thesis: p in Vertical_Line r
hence p in Vertical_Line r ; ::_thesis: verum
end;
theorem :: JORDAN6:32
for r being real number
for p being Point of (TOP-REAL 2) holds
( p in Horizontal_Line r iff p `2 = r )
proof
let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) holds
( p in Horizontal_Line r iff p `2 = r )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in Horizontal_Line r iff p `2 = r )
hereby ::_thesis: ( p `2 = r implies p in Horizontal_Line r )
assume p in Horizontal_Line r ; ::_thesis: p `2 = r
then ex q being Point of (TOP-REAL 2) st
( q = p & q `2 = r ) ;
hence p `2 = r ; ::_thesis: verum
end;
assume p `2 = r ; ::_thesis: p in Horizontal_Line r
hence p in Horizontal_Line r ; ::_thesis: verum
end;
theorem Th33: :: JORDAN6:33
for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )
assume P is being_simple_closed_curve ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
then reconsider P = P as Simple_closed_curve ;
A1: W-min P in P by SPRECT_1:13;
A2: E-max P in P by SPRECT_1:14;
W-min P <> E-max P by TOPREAL5:19;
then consider P01, P02 being non empty Subset of (TOP-REAL 2) such that
A3: P01 is_an_arc_of W-min P, E-max P and
A4: P02 is_an_arc_of W-min P, E-max P and
A5: P = P01 \/ P02 and
A6: P01 /\ P02 = {(W-min P),(E-max P)} by A1, A2, TOPREAL2:5;
reconsider P01 = P01, P02 = P02 as non empty Subset of (TOP-REAL 2) ;
A7: P01 is_an_arc_of E-max P, W-min P by A3, JORDAN5B:14;
A8: P02 is_an_arc_of E-max P, W-min P by A4, JORDAN5B:14;
reconsider P001 = P01, P002 = P02 as non empty Subset of (TOP-REAL 2) ;
A9: (E-max P) `1 = E-bound P by EUCLID:52;
A10: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;
P01 is closed by A3, COMPTS_1:7, JORDAN5A:1;
then A11: P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A10, TOPS_1:8;
A12: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6;
P02 is closed by A4, COMPTS_1:7, JORDAN5A:1;
then A13: P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, TOPS_1:8;
consider q1 being Point of (TOP-REAL 2) such that
A14: q1 in P001 and
A15: q1 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A3, Th12;
A16: (W-min P) `1 = W-bound P by EUCLID:52;
(E-max P) `1 = E-bound P by EUCLID:52;
then q1 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A15, A16;
then P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A14, XBOOLE_0:def_4;
then A17: P01 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by XBOOLE_0:def_7;
consider q2 being Point of (TOP-REAL 2) such that
A18: q2 in P002 and
A19: q2 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A4, Th12;
q2 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A9, A16, A19;
then P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A18, XBOOLE_0:def_4;
then A20: P02 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by XBOOLE_0:def_7;
percases ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ;
suppose (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A3, A5, A6, A8; ::_thesis: verum
end;
supposeA21: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
now__::_thesis:_(_(_(First_Point_(P01,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_<_(Last_Point_(P02,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_&_ex_P1,_P2_being_non_empty_Subset_of_(TOP-REAL_2)_st_
(_P1_is_an_arc_of_W-min_P,_E-max_P_&_P2_is_an_arc_of_E-max_P,_W-min_P_&_P1_/\_P2_=_{(W-min_P),(E-max_P)}_&_P1_\/_P2_=_P_&_(First_Point_(P1,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P2,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_)_or_(_(First_Point_(P01,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_=_(Last_Point_(P02,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_&_contradiction_)_)
percases ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A21, XXREAL_0:1;
caseA22: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
A23: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P01,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A3, A11, A17, JORDAN5C:18;
Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = First_Point (P02,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A4, A13, A20, JORDAN5C:18;
hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23; ::_thesis: verum
end;
caseA24: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: contradiction
set p = First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)));
set p9 = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)));
A25: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A3, A11, A17, JORDAN5C:def_1;
then A26: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 by XBOOLE_0:def_4;
First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A25, XBOOLE_0:def_4;
then A27: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;
A28: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A8, A13, A20, JORDAN5C:def_2;
then A29: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 by XBOOLE_0:def_4;
Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A28, XBOOLE_0:def_4;
then (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31;
then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A24, A27, TOPREAL3:6;
then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ P02 by A26, A29, XBOOLE_0:def_4;
then ( First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = W-min P or First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = E-max P ) by A6, TARSKI:def_2;
hence contradiction by A9, A16, A27, TOPREAL5:17; ::_thesis: verum
end;
end;
end;
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A30: P1 is_an_arc_of W-min P, E-max P and
A31: P2 is_an_arc_of E-max P, W-min P and
A32: P1 /\ P2 = {(W-min P),(E-max P)} and
A33: P1 \/ P2 = P and
A34: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ;
reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;
take P1 ; ::_thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
take P2 ; ::_thesis: ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
thus ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A30, A31, A32, A33, A34; ::_thesis: verum
end;
end;
end;
begin
theorem Th34: :: JORDAN6:34
for P being Subset of I[01] st P = the carrier of I[01] \ {0,1} holds
P is open
proof
let P be Subset of I[01]; ::_thesis: ( P = the carrier of I[01] \ {0,1} implies P is open )
assume A1: P = the carrier of I[01] \ {0,1} ; ::_thesis: P is open
A2: 0 in [.0,1.] by XXREAL_1:1;
A3: 1 in [.0,1.] by XXREAL_1:1;
reconsider Q0 = {0} as Subset of I[01] by A2, BORSUK_1:40, ZFMISC_1:31;
reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1:40, ZFMISC_1:31;
Q0 \/ Q1 is closed by A2, A3, BORSUK_1:40, TOPS_1:9;
then ([#] I[01]) \ (Q0 \/ Q1) is open by PRE_TOPC:def_3;
hence P is open by A1, ENUMSET1:1; ::_thesis: verum
end;
theorem :: JORDAN6:35
for P being Subset of R^1
for r, s being real number st P = ].r,s.[ holds
P is open
proof
let P be Subset of R^1; ::_thesis: for r, s being real number st P = ].r,s.[ holds
P is open
let r, s be real number ; ::_thesis: ( P = ].r,s.[ implies P is open )
assume A1: P = ].r,s.[ ; ::_thesis: P is open
{ r1 where r1 is Real : r < r1 } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r1 where r1 is Real : r < r1 } or x in REAL )
assume x in { r1 where r1 is Real : r < r1 } ; ::_thesis: x in REAL
then ex r1 being Real st
( r1 = x & r < r1 ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider P1 = { r1 where r1 is Real : r < r1 } as Subset of R^1 by TOPMETR:17;
{ r2 where r2 is Real : s > r2 } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r2 where r2 is Real : s > r2 } or x in REAL )
assume x in { r2 where r2 is Real : s > r2 } ; ::_thesis: x in REAL
then ex r2 being Real st
( r2 = x & s > r2 ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider P2 = { r2 where r2 is Real : s > r2 } as Subset of R^1 by TOPMETR:17;
A2: P1 is open by JORDAN2B:25;
A3: P2 is open by JORDAN2B:24;
A4: P c= P1 /\ P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 )
assume A5: x in P ; ::_thesis: x in P1 /\ P2
then reconsider r1 = x as Real by TOPMETR:17;
A6: r < r1 by A1, A5, XXREAL_1:4;
A7: r1 < s by A1, A5, XXREAL_1:4;
A8: x in P1 by A6;
x in P2 by A7;
hence x in P1 /\ P2 by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
P1 /\ P2 c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P )
assume A9: x in P1 /\ P2 ; ::_thesis: x in P
then A10: x in P1 by XBOOLE_0:def_4;
A11: x in P2 by A9, XBOOLE_0:def_4;
A12: ex r1 being Real st
( r1 = x & r < r1 ) by A10;
ex r2 being Real st
( r2 = x & s > r2 ) by A11;
hence x in P by A1, A12, XXREAL_1:4; ::_thesis: verum
end;
then P = P1 /\ P2 by A4, XBOOLE_0:def_10;
hence P is open by A2, A3, TOPS_1:11; ::_thesis: verum
end;
theorem Th36: :: JORDAN6:36
for P7 being Subset of I[01] st P7 = the carrier of I[01] \ {0,1} holds
( P7 <> {} & P7 is connected )
proof
let P7 be Subset of I[01]; ::_thesis: ( P7 = the carrier of I[01] \ {0,1} implies ( P7 <> {} & P7 is connected ) )
assume A1: P7 = the carrier of I[01] \ {0,1} ; ::_thesis: ( P7 <> {} & P7 is connected )
A2: 1 / 2 in [.0,1.] by XXREAL_1:1;
A3: not 1 / 2 in {0,1} by TARSKI:def_2;
A4: [#] (I[01] | P7) = P7 by PRE_TOPC:def_5;
for A, B being Subset of (I[01] | P7) st [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open holds
A meets B
proof
let A, B be Subset of (I[01] | P7); ::_thesis: ( [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open implies A meets B )
assume that
A5: [#] (I[01] | P7) = A \/ B and
A6: A <> {} (I[01] | P7) and
A7: B <> {} (I[01] | P7) and
A8: A is open and
A9: B is open ; ::_thesis: A meets B
assume A10: A misses B ; ::_thesis: contradiction
A11: ].0,1.[ misses {0,1} by XXREAL_1:86;
A12: P7 = (].0,1.[ \/ {0,1}) \ {0,1} by A1, BORSUK_1:40, XXREAL_1:128
.= ].0,1.[ \ {0,1} by XBOOLE_1:40
.= ].0,1.[ by A11, XBOOLE_1:83 ;
reconsider D1 = [.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider P1 = P7 as Subset of R^1 by A12, TOPMETR:17;
I[01] = R^1 | D1 by TOPMETR:19, TOPMETR:20;
then A13: I[01] | P7 = R^1 | P1 by BORSUK_1:40, PRE_TOPC:7;
P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) } by A12, RCOMP_1:def_2;
then P1 is open by JORDAN2B:26;
then A14: I[01] | P7 is non empty open SubSpace of R^1 by A1, A2, A3, A4, A13, BORSUK_1:40, TSEP_1:16, XBOOLE_0:def_5;
reconsider P = A, Q = B as non empty Subset of REAL by A4, A6, A7, A12, XBOOLE_1:1;
reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6;
A15: A0 is open by A8, A14, TSEP_1:17;
A16: B0 is open by A9, A14, TSEP_1:17;
set xp = the Element of P;
reconsider xp = the Element of P as Real ;
A17: xp in P ;
0 is LowerBound of P
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in P or 0 <= r )
assume r in P ; ::_thesis: 0 <= r
then r in ].0,1.[ by A4, A12;
then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def_2;
then ex u being Real st
( u = r & 0 < u & u < 1 ) ;
hence 0 <= r ; ::_thesis: verum
end;
then A18: P is bounded_below by XXREAL_2:def_9;
0 is LowerBound of Q
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Q or 0 <= r )
assume r in Q ; ::_thesis: 0 <= r
then r in ].0,1.[ by A4, A12;
then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def_2;
then ex u being Real st
( u = r & 0 < u & u < 1 ) ;
hence 0 <= r ; ::_thesis: verum
end;
then A19: Q is bounded_below by XXREAL_2:def_9;
reconsider l = lower_bound Q as Element of REAL ;
reconsider m = l as Point of RealSpace by METRIC_1:def_13;
reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6;
A20: not l in Q
proof
assume l in Q ; ::_thesis: contradiction
then consider s being real number such that
A21: s > 0 and
A22: Ball (m,s) c= B0 by A16, TOPMETR:15, TOPMETR:def_6;
reconsider s = s as Element of REAL by XREAL_0:def_1;
reconsider e1 = l - (s / 2) as Point of RealSpace by METRIC_1:def_13;
s / 2 < s by A21, XREAL_1:216;
then abs (l - (l - (s / 2))) < s by A21, ABSVALUE:def_1;
then the distance of RealSpace . (m,e1) < s by METRIC_1:def_12, METRIC_1:def_13;
then dist (m,e1) < s by METRIC_1:def_1;
then e1 in { z where z is Element of RealSpace : dist (m,z) < s } ;
then l - (s / 2) in Ball (m,s) by METRIC_1:17;
then l <= l - (s / 2) by A19, A22, SEQ_4:def_2;
then l + (s / 2) <= l by XREAL_1:19;
then (l + (s / 2)) - l <= l - l by XREAL_1:9;
hence contradiction by A21, XREAL_1:139; ::_thesis: verum
end;
A23: now__::_thesis:_not_l_<=_0
assume A24: l <= 0 ; ::_thesis: contradiction
0 < xp by A4, A12, A17, XXREAL_1:4;
then consider r5 being real number such that
A25: r5 in Q and
A26: r5 < l + (xp - l) by A19, A24, SEQ_4:def_2;
reconsider r5 = r5 as Real by XREAL_0:def_1;
A27: { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } c= P
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } or y in P )
assume y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ; ::_thesis: y in P
then ex s5 being Real st
( s5 = y & s5 in P & r5 < s5 ) ;
hence y in P ; ::_thesis: verum
end;
then reconsider P5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } as Subset of REAL by XBOOLE_1:1;
A28: xp in P5 by A26;
A29: P5 is bounded_below by A18, A27, XXREAL_2:44;
reconsider l5 = lower_bound P5 as Real ;
reconsider m5 = l5 as Point of RealSpace by METRIC_1:def_13;
A30: now__::_thesis:_not_l5_<=_r5
assume A31: l5 <= r5 ; ::_thesis: contradiction
now__::_thesis:_not_l5_<_r5
assume l5 < r5 ; ::_thesis: contradiction
then r5 - l5 > 0 by XREAL_1:50;
then consider r being real number such that
A32: r in P5 and
A33: r < l5 + (r5 - l5) by A28, A29, SEQ_4:def_2;
ex s6 being Real st
( s6 = r & s6 in P & r5 < s6 ) by A32;
hence contradiction by A33; ::_thesis: verum
end;
then l5 = r5 by A31, XXREAL_0:1;
then consider r7 being real number such that
A34: r7 > 0 and
A35: Ball (m5,r7) c= B0 by A16, A25, TOPMETR:15, TOPMETR:def_6;
consider r9 being real number such that
A36: r9 in P5 and
A37: r9 < l5 + r7 by A28, A29, A34, SEQ_4:def_2;
reconsider r9 = r9 as Real by XREAL_0:def_1;
reconsider e8 = r9 as Point of RealSpace by METRIC_1:def_13;
l5 <= r9 by A29, A36, SEQ_4:def_2;
then A38: r9 - l5 >= 0 by XREAL_1:48;
r9 - l5 < (l5 + r7) - l5 by A37, XREAL_1:9;
then abs (r9 - l5) < r7 by A38, ABSVALUE:def_1;
then the distance of RealSpace . (e8,m5) < r7 by METRIC_1:def_12, METRIC_1:def_13;
then dist (e8,m5) < r7 by METRIC_1:def_1;
then e8 in { z where z is Element of RealSpace : dist (m5,z) < r7 } ;
then e8 in Ball (m5,r7) by METRIC_1:17;
hence contradiction by A10, A27, A35, A36, XBOOLE_0:3; ::_thesis: verum
end;
A39: 0 < r5 by A4, A12, A25, XXREAL_1:4;
A40: l5 - r5 > 0 by A30, XREAL_1:50;
set q = the Element of P5;
A41: the Element of P5 in P5 by A28;
then reconsider q1 = the Element of P5 as Real ;
q1 in P by A27, A41;
then A42: q1 < 1 by A4, A12, XXREAL_1:4;
l5 <= q1 by A28, A29, SEQ_4:def_2;
then l5 < 1 by A42, XXREAL_0:2;
then l5 in ].0,1.[ by A30, A39, XXREAL_1:4;
then A43: ( l5 in P or l5 in Q ) by A4, A5, A12, XBOOLE_0:def_3;
now__::_thesis:_not_l5_in_P
assume l5 in P ; ::_thesis: contradiction
then consider s5 being real number such that
A44: s5 > 0 and
A45: Ball (m5,s5) c= P by A15, TOPMETR:15, TOPMETR:def_6;
reconsider s5 = s5 as Element of REAL by XREAL_0:def_1;
set s59 = min (s5,(l5 - r5));
A46: min (s5,(l5 - r5)) > 0 by A40, A44, XXREAL_0:21;
A47: min (s5,(l5 - r5)) <= s5 by XXREAL_0:17;
A48: (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;
min (s5,(l5 - r5)) <= l5 - r5 by XXREAL_0:17;
then (min (s5,(l5 - r5))) / 2 < l5 - r5 by A48, XXREAL_0:2;
then ((min (s5,(l5 - r5))) / 2) + r5 < (l5 - r5) + r5 by XREAL_1:6;
then A49: (((min (s5,(l5 - r5))) / 2) + r5) - ((min (s5,(l5 - r5))) / 2) < l5 - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;
reconsider e1 = l5 - ((min (s5,(l5 - r5))) / 2) as Point of RealSpace by METRIC_1:def_13;
(min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216;
then (min (s5,(l5 - r5))) / 2 < s5 by A47, XXREAL_0:2;
then abs (l5 - (l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by A46, ABSVALUE:def_1;
then real_dist . (l5,(l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by METRIC_1:def_12;
then dist (m5,e1) < s5 by METRIC_1:def_1, METRIC_1:def_13;
then e1 in { z where z is Element of RealSpace : dist (m5,z) < s5 } ;
then l5 - ((min (s5,(l5 - r5))) / 2) in Ball (m5,s5) by METRIC_1:17;
then A50: l5 - ((min (s5,(l5 - r5))) / 2) in { s7 where s7 is Real : ( s7 in P & r5 < s7 ) } by A45, A49;
l5 < l5 + ((min (s5,(l5 - r5))) / 2) by A46, XREAL_1:29, XREAL_1:139;
then l5 - ((min (s5,(l5 - r5))) / 2) < (l5 + ((min (s5,(l5 - r5))) / 2)) - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9;
hence contradiction by A29, A50, SEQ_4:def_2; ::_thesis: verum
end;
then consider s1 being real number such that
A51: s1 > 0 and
A52: Ball (m5,s1) c= B0 by A16, A43, TOPMETR:15, TOPMETR:def_6;
s1 / 2 > 0 by A51, XREAL_1:139;
then consider r2 being real number such that
A53: r2 in P5 and
A54: r2 < l5 + (s1 / 2) by A28, A29, SEQ_4:def_2;
reconsider r2 = r2 as Real by XREAL_0:def_1;
A55: l5 <= r2 by A29, A53, SEQ_4:def_2;
reconsider s3 = r2 - l5 as Real ;
reconsider e1 = l5 + s3 as Point of RealSpace by METRIC_1:def_13;
A56: r2 - l5 >= 0 by A55, XREAL_1:48;
A57: r2 - l5 < (l5 + (s1 / 2)) - l5 by A54, XREAL_1:14;
s1 / 2 < s1 by A51, XREAL_1:216;
then A58: (l5 + s3) - l5 < s1 by A57, XXREAL_0:2;
abs ((l5 + s3) - l5) = (l5 + s3) - l5 by A56, ABSVALUE:def_1;
then real_dist . ((l5 + s3),l5) < s1 by A58, METRIC_1:def_12;
then dist (e1,m5) < s1 by METRIC_1:def_1, METRIC_1:def_13;
then l5 + s3 in { z where z is Element of RealSpace : dist (m5,z) < s1 } ;
then l5 + s3 in Ball (m5,s1) by METRIC_1:17;
then A59: l5 + s3 in P5 /\ Q by A52, A53, XBOOLE_0:def_4;
P5 /\ Q c= P /\ Q by A27, XBOOLE_1:26;
hence contradiction by A10, A59, XBOOLE_0:def_7; ::_thesis: verum
end;
set q = the Element of Q;
A60: the Element of Q in Q ;
reconsider q1 = the Element of Q as Real ;
A61: q1 < 1 by A4, A12, A60, XXREAL_1:4;
l <= q1 by A19, SEQ_4:def_2;
then l < 1 by A61, XXREAL_0:2;
then l in ].0,1.[ by A23, XXREAL_1:4;
then A62: t in A0 by A4, A5, A12, A20, XBOOLE_0:def_3;
A0 is open by A8, A14, TSEP_1:17;
then consider s1 being real number such that
A63: s1 > 0 and
A64: Ball (m,s1) c= A0 by A62, TOPMETR:15, TOPMETR:def_6;
s1 / 2 > 0 by A63, XREAL_1:139;
then consider r2 being real number such that
A65: r2 in Q and
A66: r2 < l + (s1 / 2) by A19, SEQ_4:def_2;
reconsider r2 = r2 as Real by XREAL_0:def_1;
A67: l <= r2 by A19, A65, SEQ_4:def_2;
set s3 = r2 - l;
reconsider e1 = l + (r2 - l) as Point of RealSpace by METRIC_1:def_13;
A68: r2 - l >= 0 by A67, XREAL_1:48;
A69: r2 - l < (l + (s1 / 2)) - l by A66, XREAL_1:14;
s1 / 2 < s1 by A63, XREAL_1:216;
then A70: (l + (r2 - l)) - l < s1 by A69, XXREAL_0:2;
abs ((l + (r2 - l)) - l) = (l + (r2 - l)) - l by A68, ABSVALUE:def_1;
then real_dist . ((l + (r2 - l)),l) < s1 by A70, METRIC_1:def_12;
then dist (e1,m) < s1 by METRIC_1:def_1, METRIC_1:def_13;
then l + (r2 - l) in { z where z is Element of RealSpace : dist (m,z) < s1 } ;
then l + (r2 - l) in Ball (m,s1) by METRIC_1:17;
hence contradiction by A10, A64, A65, XBOOLE_0:3; ::_thesis: verum
end;
then I[01] | P7 is connected by CONNSP_1:11;
hence ( P7 <> {} & P7 is connected ) by A1, A2, A3, BORSUK_1:40, CONNSP_1:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th37: :: JORDAN6:37
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies p1 <> p2 )
assume P is_an_arc_of p1,p2 ; ::_thesis: p1 <> p2
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A1: f is being_homeomorphism and
A2: f . 0 = p1 and
A3: f . 1 = p2 by TOPREAL1:def_1;
1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then A4: 1 in dom f by A1, TOPS_2:def_5;
A5: f is one-to-one by A1, TOPS_2:def_5;
0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then 0 in dom f by A1, TOPS_2:def_5;
hence p1 <> p2 by A2, A3, A4, A5, FUNCT_1:def_4; ::_thesis: verum
end;
theorem :: JORDAN6:38
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open
let P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open
let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is open )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q = P \ {p1,p2} ; ::_thesis: Q is open
reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL n) | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by A1, TOPREAL1:def_1;
reconsider f1 = f as Function ;
A6: f " is being_homeomorphism by A3, TOPS_2:56;
reconsider g = f " as Function of ((TOP-REAL n) | P),I[01] ;
reconsider g1 = g as Function ;
reconsider R = the carrier of I[01] \ {0,1} as Subset of I[01] ;
A7: [#] I[01] <> {} ;
A8: R is open by Th34;
A9: f is one-to-one by A3, TOPS_2:def_5;
A10: g is one-to-one by A6, TOPS_2:def_5;
A11: g is continuous by A3, TOPS_2:def_5;
A12: [#] I[01] = dom f by A3, TOPS_2:def_5;
0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then A13: 0 in dom f by A3, TOPS_2:def_5;
1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then A14: 1 in dom f by A3, TOPS_2:def_5;
rng f = [#] ((TOP-REAL n) | P) by A3, TOPS_2:def_5;
then A15: (f ") " = f by A9, TOPS_2:51;
rng g = [#] I[01] by A6, TOPS_2:def_5;
then g is onto by FUNCT_2:def_3;
then A16: g1 " = f1 by A10, A15, TOPS_2:def_4;
g " R = (g1 " the carrier of I[01]) \ (g1 " {0,1}) by FUNCT_1:69
.= ((g1 ") .: the carrier of I[01]) \ (g1 " {0,1}) by A10, FUNCT_1:85
.= (f1 .: ([#] I[01])) \ (f1 .: {0,1}) by A10, A16, FUNCT_1:85
.= (rng f) \ (f .: {0,1}) by A12, RELAT_1:113
.= ([#] ((TOP-REAL n) | P)) \ (f .: {0,1}) by A3, TOPS_2:def_5
.= P \ (f .: {0,1}) by PRE_TOPC:def_5
.= Q by A2, A4, A5, A13, A14, FUNCT_1:60 ;
hence Q is open by A7, A8, A11, TOPS_2:43; ::_thesis: verum
end;
theorem Th39: :: JORDAN6:39
for n being Element of NAT
for P, P1, P2 being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
proof
let n be Element of NAT ; ::_thesis: for P, P1, P2 being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let P, P1, P2 be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} implies Q is open )
assume that
A1: P2 is_an_arc_of p1,p2 and
A2: P1 \/ P2 = P and
A3: P1 /\ P2 = {p1,p2} and
A4: Q = P1 \ {p1,p2} ; ::_thesis: Q is open
reconsider P21 = P2 as Subset of (TOP-REAL n) ;
A5: P21 is compact by A1, JORDAN5A:1;
p1 in P1 /\ P2 by A3, TARSKI:def_2;
then A6: p1 in P2 by XBOOLE_0:def_4;
A7: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5;
then reconsider P29 = P21 as Subset of ((TOP-REAL n) | P) by A2, XBOOLE_1:7;
p2 in P1 /\ P2 by A3, TARSKI:def_2;
then A8: p2 in P2 by XBOOLE_0:def_4;
P29 is compact by A5, A7, COMPTS_1:2;
then A9: P29 is closed by COMPTS_1:7;
A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A2, XBOOLE_1:42
.= (P1 \ P2) \/ {} by XBOOLE_1:37
.= P1 \ P2 ;
A11: P1 \ P2 c= Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 \ P2 or x in Q )
assume A12: x in P1 \ P2 ; ::_thesis: x in Q
then A13: x in P1 by XBOOLE_0:def_5;
not x in P2 by A12, XBOOLE_0:def_5;
then not x in {p1,p2} by A6, A8, TARSKI:def_2;
hence x in Q by A4, A13, XBOOLE_0:def_5; ::_thesis: verum
end;
Q c= P1 \ P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in P1 \ P2 )
assume A14: x in Q ; ::_thesis: x in P1 \ P2
then A15: x in P1 by A4, XBOOLE_0:def_5;
not x in {p1,p2} by A4, A14, XBOOLE_0:def_5;
then not x in P2 by A3, A15, XBOOLE_0:def_4;
hence x in P1 \ P2 by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
then P1 \ P2 = Q by A11, XBOOLE_0:def_10;
then Q = P29 ` by A7, A10, SUBSET_1:def_4;
hence Q is open by A9, TOPS_1:3; ::_thesis: verum
end;
theorem Th40: :: JORDAN6:40
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is connected )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q = P \ {p1,p2} ; ::_thesis: Q is connected
reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL n) | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by A1, TOPREAL1:def_1;
reconsider P7 = the carrier of I[01] \ {0,1} as Subset of I[01] ;
A6: f is continuous by A3, TOPS_2:def_5;
A7: f is one-to-one by A3, TOPS_2:def_5;
Q = f .: P7
proof
[#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5;
then A8: rng f = P by A3, TOPS_2:def_5;
thus Q c= f .: P7 :: according to XBOOLE_0:def_10 ::_thesis: f .: P7 c= Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in f .: P7 )
assume A9: x in Q ; ::_thesis: x in f .: P7
then A10: x in P by A2, XBOOLE_0:def_5;
A11: not x in {p1,p2} by A2, A9, XBOOLE_0:def_5;
consider z being set such that
A12: z in dom f and
A13: x = f . z by A8, A10, FUNCT_1:def_3;
now__::_thesis:_not_z_in_{0,1}
assume z in {0,1} ; ::_thesis: contradiction
then ( x = p1 or x = p2 ) by A4, A5, A13, TARSKI:def_2;
hence contradiction by A11, TARSKI:def_2; ::_thesis: verum
end;
then z in P7 by A12, XBOOLE_0:def_5;
hence x in f .: P7 by A12, A13, FUNCT_1:def_6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: P7 or y in Q )
assume y in f .: P7 ; ::_thesis: y in Q
then consider x being set such that
A14: x in dom f and
A15: x in P7 and
A16: y = f . x by FUNCT_1:def_6;
A17: not x in {0,1} by A15, XBOOLE_0:def_5;
then A18: x <> 0 by TARSKI:def_2;
A19: x <> 1 by A17, TARSKI:def_2;
A20: y in P by A8, A14, A16, FUNCT_1:def_3;
now__::_thesis:_not_y_in_{p1,p2}
assume A21: y in {p1,p2} ; ::_thesis: contradiction
reconsider f1 = f as Function of the carrier of I[01], the carrier of ((TOP-REAL n) | P9) ;
now__::_thesis:_(_(_f_._x_=_p1_&_contradiction_)_or_(_f_._x_=_p2_&_contradiction_)_)
percases ( f . x = p1 or f . x = p2 ) by A16, A21, TARSKI:def_2;
caseA22: f . x = p1 ; ::_thesis: contradiction
dom f1 = the carrier of I[01] by FUNCT_2:def_1;
then 0 in dom f1 by BORSUK_1:40, XXREAL_1:1;
hence contradiction by A4, A7, A14, A18, A22, FUNCT_1:def_4; ::_thesis: verum
end;
caseA23: f . x = p2 ; ::_thesis: contradiction
dom f1 = the carrier of I[01] by FUNCT_2:def_1;
then 1 in dom f1 by BORSUK_1:40, XXREAL_1:1;
hence contradiction by A5, A7, A14, A19, A23, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence y in Q by A2, A20, XBOOLE_0:def_5; ::_thesis: verum
end;
hence Q is connected by A6, Th36, TOPS_2:61; ::_thesis: verum
end;
theorem Th41: :: JORDAN6:41
for GX being TopSpace
for P1, P being Subset of GX
for Q9 being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
proof
let GX be TopSpace; ::_thesis: for P1, P being Subset of GX
for Q9 being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let P1, P be Subset of GX; ::_thesis: for Q9 being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let Q9 be Subset of (GX | P1); ::_thesis: for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds
Q is connected
let Q be Subset of (GX | P); ::_thesis: ( P1 c= P & Q = Q9 & Q9 is connected implies Q is connected )
assume that
A1: P1 c= P and
A2: Q = Q9 and
A3: Q9 is connected ; ::_thesis: Q is connected
[#] (GX | P) = P by PRE_TOPC:def_5;
then reconsider P19 = P1 as Subset of (GX | P) by A1;
GX | P1 = (GX | P) | P19 by A1, PRE_TOPC:7;
hence Q is connected by A2, A3, CONNSP_1:23; ::_thesis: verum
end;
theorem Th42: :: JORDAN6:42
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 )
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 )
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 ) )
assume P is_an_arc_of p1,p2 ; ::_thesis: ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 )
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A1: f is being_homeomorphism and
A2: f . 0 = p1 and
A3: f . 1 = p2 by TOPREAL1:def_1;
1 / 2 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then A4: 1 / 2 in dom f by A1, TOPS_2:def_5;
then f . (1 / 2) in rng f by FUNCT_1:def_3;
then f . (1 / 2) in the carrier of ((TOP-REAL n) | P) ;
then A5: f . (1 / 2) in P by PRE_TOPC:8;
then reconsider p = f . (1 / 2) as Point of (TOP-REAL n) ;
A6: f is one-to-one by A1, TOPS_2:def_5;
0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then 0 in dom f by A1, TOPS_2:def_5;
then A7: p1 <> p by A2, A4, A6, FUNCT_1:def_4;
1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then 1 in dom f by A1, TOPS_2:def_5;
then f . 1 <> f . (1 / 2) by A4, A6, FUNCT_1:def_4;
hence ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 ) by A3, A5, A7; ::_thesis: verum
end;
theorem :: JORDAN6:43
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies P \ {p1,p2} <> {} )
assume P is_an_arc_of p1,p2 ; ::_thesis: P \ {p1,p2} <> {}
then consider p3 being Point of (TOP-REAL n) such that
A1: p3 in P and
A2: p3 <> p1 and
A3: p3 <> p2 by Th42;
not p3 in {p1,p2} by A2, A3, TARSKI:def_2;
hence P \ {p1,p2} <> {} by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: JORDAN6:44
for n being Element of NAT
for P1, P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds
Q is connected
proof
let n be Element of NAT ; ::_thesis: for P1, P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds
Q is connected
let P1, P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds
Q is connected
let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds
Q is connected
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} implies Q is connected )
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P1 c= P and
A3: Q = P1 \ {p1,p2} ; ::_thesis: Q is connected
[#] ((TOP-REAL n) | P1) = P1 by PRE_TOPC:def_5;
then reconsider Q9 = Q as Subset of ((TOP-REAL n) | P1) by A3, XBOOLE_1:36;
Q9 is connected by A1, A3, Th40;
hence Q is connected by A2, Th41; ::_thesis: verum
end;
theorem Th45: :: JORDAN6:45
for T, S, V being non empty TopSpace
for P1 being non empty Subset of S
for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
proof
let T, S, V be non empty TopSpace; ::_thesis: for P1 being non empty Subset of S
for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let P1 be non empty Subset of S; ::_thesis: for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let P2 be Subset of S; ::_thesis: for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let f be Function of T,(S | P1); ::_thesis: for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )
let g be Function of (S | P2),V; ::_thesis: ( P1 c= P2 & f is continuous & g is continuous implies ex h being Function of T,V st
( h = g * f & h is continuous ) )
assume that
A1: P1 c= P2 and
A2: f is continuous and
A3: g is continuous ; ::_thesis: ex h being Function of T,V st
( h = g * f & h is continuous )
reconsider P3 = P2 as non empty Subset of S by A1, XBOOLE_1:3;
A4: [#] (S | P1) = P1 by PRE_TOPC:def_5;
A5: [#] (S | P2) = P2 by PRE_TOPC:def_5;
then reconsider f1 = f as Function of T,(S | P3) by A1, A4, FUNCT_2:7;
for F1 being Subset of (S | P2) st F1 is closed holds
f1 " F1 is closed
proof
let F1 be Subset of (S | P2); ::_thesis: ( F1 is closed implies f1 " F1 is closed )
assume A6: F1 is closed ; ::_thesis: f1 " F1 is closed
reconsider P19 = P1 as non empty Subset of (S | P3) by A1, A5;
A7: [#] (S | P1) = P1 by PRE_TOPC:def_5;
reconsider P4 = F1 /\ P19 as Subset of ((S | P3) | P19) by TOPS_2:29;
A8: S | P1 = (S | P3) | P19 by A1, PRE_TOPC:7;
A9: P4 is closed by A6, Th2;
f1 " P1 = the carrier of T by A7, FUNCT_2:40
.= dom f1 by FUNCT_2:def_1 ;
then f1 " F1 = (f1 " F1) /\ (f1 " P1) by RELAT_1:132, XBOOLE_1:28
.= f " P4 by FUNCT_1:68 ;
hence f1 " F1 is closed by A2, A8, A9, PRE_TOPC:def_6; ::_thesis: verum
end;
then f1 is continuous by PRE_TOPC:def_6;
hence ex h being Function of T,V st
( h = g * f & h is continuous ) by A3; ::_thesis: verum
end;
theorem Th46: :: JORDAN6:46
for n being Element of NAT
for P1, P2 being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
proof
let n be Element of NAT ; ::_thesis: for P1, P2 being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let P1, P2 be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 implies P1 = P2 )
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P2 is_an_arc_of p1,p2 and
A3: P1 c= P2 ; ::_thesis: P1 = P2
reconsider P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL n) by A1, A2, TOPREAL1:1;
now__::_thesis:_not_P2_\_P1_<>_{}
assume A4: P2 \ P1 <> {} ; ::_thesis: contradiction
set p = the Element of P2 \ P1;
A5: the Element of P2 \ P1 in P2 by A4, XBOOLE_0:def_5;
A6: not the Element of P2 \ P1 in P1 by A4, XBOOLE_0:def_5;
consider f1 being Function of I[01],((TOP-REAL n) | P19) such that
A7: f1 is being_homeomorphism and
A8: f1 . 0 = p1 and
A9: f1 . 1 = p2 by A1, TOPREAL1:def_1;
A10: f1 is continuous by A7, TOPS_2:def_5;
consider f2 being Function of I[01],((TOP-REAL n) | P29) such that
A11: f2 is being_homeomorphism and
A12: f2 . 0 = p1 and
A13: f2 . 1 = p2 by A2, TOPREAL1:def_1;
reconsider f4 = f2 as Function ;
A14: f2 is one-to-one by A11, TOPS_2:def_5;
A15: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def_5;
A16: f2 " is being_homeomorphism by A11, TOPS_2:56;
then A17: dom (f2 ") = [#] ((TOP-REAL n) | P2) by TOPS_2:def_5
.= P2 by PRE_TOPC:def_5 ;
f2 " is continuous by A11, TOPS_2:def_5;
then consider h being Function of I[01],I[01] such that
A18: h = (f2 ") * f1 and
A19: h is continuous by A3, A10, Th45;
reconsider h1 = h as Function of (Closed-Interval-TSpace (0,1)),R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17, TOPMETR:20;
for F1 being Subset of R^1 st F1 is closed holds
h1 " F1 is closed
proof
let F1 be Subset of R^1; ::_thesis: ( F1 is closed implies h1 " F1 is closed )
assume A20: F1 is closed ; ::_thesis: h1 " F1 is closed
reconsider K = the carrier of I[01] as Subset of R^1 by BORSUK_1:40, TOPMETR:17;
A21: I[01] = R^1 | K by BORSUK_1:40, TOPMETR:19, TOPMETR:20;
reconsider P3 = F1 /\ K as Subset of (R^1 | K) by TOPS_2:29;
A22: P3 is closed by A20, Th2;
h1 " K = the carrier of I[01] by FUNCT_2:40
.= dom h1 by FUNCT_2:def_1 ;
then h1 " F1 = (h1 " F1) /\ (h1 " K) by RELAT_1:132, XBOOLE_1:28
.= h " P3 by FUNCT_1:68 ;
hence h1 " F1 is closed by A19, A21, A22, PRE_TOPC:def_6, TOPMETR:20; ::_thesis: verum
end;
then reconsider g = h1 as continuous Function of (Closed-Interval-TSpace (0,1)),R^1 by PRE_TOPC:def_6;
A23: dom f1 = [#] I[01] by A7, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then A24: 0 in dom f1 by XXREAL_1:1;
A25: 1 in dom f1 by A23, XXREAL_1:1;
A26: g . 0 = (f2 ") . p1 by A8, A18, A24, FUNCT_1:13;
A27: g . 1 = (f2 ") . p2 by A9, A18, A25, FUNCT_1:13;
A28: dom f2 = [#] I[01] by A11, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then A29: 0 in dom f2 by XXREAL_1:1;
A30: 1 in dom f2 by A28, XXREAL_1:1;
A31: f2 is onto by A15, FUNCT_2:def_3;
then A32: (f2 ") . p1 = (f4 ") . p1 by A14, TOPS_2:def_4;
A33: (f2 ") . p2 = (f4 ") . p2 by A14, A31, TOPS_2:def_4;
A34: g . 0 = 0 by A12, A14, A26, A29, A32, FUNCT_1:32;
A35: g . 1 = 1 by A13, A14, A27, A30, A33, FUNCT_1:32;
the Element of P2 \ P1 in the carrier of ((TOP-REAL n) | P29) by A5, PRE_TOPC:8;
then A36: (f2 ") . the Element of P2 \ P1 in the carrier of I[01] by FUNCT_2:5;
A37: now__::_thesis:_not_(f2_")_._the_Element_of_P2_\_P1_in_rng_g
assume (f2 ") . the Element of P2 \ P1 in rng g ; ::_thesis: contradiction
then consider x being set such that
A38: x in dom g and
A39: (f2 ") . the Element of P2 \ P1 = g . x by FUNCT_1:def_3;
A40: (f2 ") . the Element of P2 \ P1 = (f2 ") . (f1 . x) by A18, A38, A39, FUNCT_1:12;
A41: x in dom f1 by A18, A38, FUNCT_1:11;
A42: f1 . x in dom (f2 ") by A18, A38, FUNCT_1:11;
f2 " is one-to-one by A16, TOPS_2:def_5;
then the Element of P2 \ P1 = f1 . x by A5, A17, A40, A42, FUNCT_1:def_4;
then A43: the Element of P2 \ P1 in rng f1 by A41, FUNCT_1:def_3;
rng f1 = [#] ((TOP-REAL n) | P1) by A7, TOPS_2:def_5
.= P1 by PRE_TOPC:def_5 ;
hence contradiction by A4, A43, XBOOLE_0:def_5; ::_thesis: verum
end;
reconsider r = (f2 ") . the Element of P2 \ P1 as Real by A36, BORSUK_1:40;
A44: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def_5
.= P2 by PRE_TOPC:def_5 ;
A45: r <= 1 by A36, BORSUK_1:40, XXREAL_1:1;
A46: now__::_thesis:_not_r_=_0
assume A47: r = 0 ; ::_thesis: contradiction
f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def_4
.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;
hence contradiction by A1, A6, A12, A47, TOPREAL1:1; ::_thesis: verum
end;
A48: now__::_thesis:_not_r_=_1
assume A49: r = 1 ; ::_thesis: contradiction
f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def_4
.= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ;
hence contradiction by A1, A6, A13, A49, TOPREAL1:1; ::_thesis: verum
end;
A50: 0 < r by A36, A46, BORSUK_1:40, XXREAL_1:1;
r < 1 by A45, A48, XXREAL_0:1;
then consider rc being Real such that
A51: g . rc = r and
A52: 0 < rc and
A53: rc < 1 by A34, A35, A50, TOPREAL5:6;
the carrier of ((TOP-REAL n) | P1) = [#] ((TOP-REAL n) | P1)
.= P1 by PRE_TOPC:def_5 ;
then rng f1 c= dom (f2 ") by A3, A17, XBOOLE_1:1;
then dom g = dom f1 by A18, RELAT_1:27
.= [#] I[01] by A7, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then rc in dom g by A52, A53, XXREAL_1:1;
hence contradiction by A37, A51, FUNCT_1:def_3; ::_thesis: verum
end;
then P2 c= P1 by XBOOLE_1:37;
hence P1 = P2 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th47: :: JORDAN6:47
for P being Subset of (TOP-REAL 2)
for Q being Subset of ((TOP-REAL 2) | P)
for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for Q being Subset of ((TOP-REAL 2) | P)
for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected
let Q be Subset of ((TOP-REAL 2) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} implies not Q is connected )
assume that
A1: P is being_simple_closed_curve and
A2: p1 in P and
A3: p2 in P and
A4: p1 <> p2 and
A5: Q = P \ {p1,p2} ; ::_thesis: not Q is connected
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A6: P1 is_an_arc_of p1,p2 and
A7: P2 is_an_arc_of p1,p2 and
A8: P = P1 \/ P2 and
A9: P1 /\ P2 = {p1,p2} by A1, A2, A3, A4, TOPREAL2:5;
A10: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
reconsider P = P as Simple_closed_curve by A1;
A11: P1 c= P by A8, XBOOLE_1:7;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider P19 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A11, XBOOLE_1:1;
A12: P2 c= P by A8, XBOOLE_1:7;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider P29 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A12, XBOOLE_1:1;
A13: P19 is open by A7, A8, A9, Th39;
A14: P29 is open by A6, A8, A9, Th39;
A15: Q c= P19 \/ P29
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in P19 \/ P29 )
assume A16: x in Q ; ::_thesis: x in P19 \/ P29
then A17: x in P by A5, XBOOLE_0:def_5;
now__::_thesis:_(_(_x_in_P1_&_not_x_in_{p1,p2}_&_x_in_P19_\/_P29_)_or_(_x_in_P2_&_not_x_in_{p1,p2}_&_x_in_P19_\/_P29_)_)
percases ( ( x in P1 & not x in {p1,p2} ) or ( x in P2 & not x in {p1,p2} ) ) by A5, A8, A16, A17, XBOOLE_0:def_3, XBOOLE_0:def_5;
case ( x in P1 & not x in {p1,p2} ) ; ::_thesis: x in P19 \/ P29
then x in P19 by XBOOLE_0:def_5;
hence x in P19 \/ P29 by XBOOLE_0:def_3; ::_thesis: verum
end;
case ( x in P2 & not x in {p1,p2} ) ; ::_thesis: x in P19 \/ P29
then x in P29 by XBOOLE_0:def_5;
hence x in P19 \/ P29 by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence x in P19 \/ P29 ; ::_thesis: verum
end;
consider p3 being Point of (TOP-REAL 2) such that
A18: p3 in P1 and
A19: p3 <> p1 and
A20: p3 <> p2 by A6, Th42;
not p3 in {p1,p2} by A19, A20, TARSKI:def_2;
then A21: P19 <> {} by A18, XBOOLE_0:def_5;
P19 c= Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P19 or x in Q )
assume A22: x in P19 ; ::_thesis: x in Q
then A23: x in P1 by XBOOLE_0:def_5;
A24: not x in {p1,p2} by A22, XBOOLE_0:def_5;
x in P by A8, A23, XBOOLE_0:def_3;
hence x in Q by A5, A24, XBOOLE_0:def_5; ::_thesis: verum
end;
then P19 /\ Q <> {} by A21, XBOOLE_1:28;
then A25: P19 meets Q by XBOOLE_0:def_7;
consider p39 being Point of (TOP-REAL 2) such that
A26: p39 in P2 and
A27: p39 <> p1 and
A28: p39 <> p2 by A7, Th42;
not p39 in {p1,p2} by A27, A28, TARSKI:def_2;
then A29: P29 <> {} by A26, XBOOLE_0:def_5;
P29 c= Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P29 or x in Q )
assume A30: x in P29 ; ::_thesis: x in Q
then A31: x in P2 by XBOOLE_0:def_5;
A32: not x in {p1,p2} by A30, XBOOLE_0:def_5;
x in P1 \/ P2 by A31, XBOOLE_0:def_3;
hence x in Q by A5, A8, A32, XBOOLE_0:def_5; ::_thesis: verum
end;
then P29 /\ Q <> {} by A29, XBOOLE_1:28;
then A33: P29 meets Q by XBOOLE_0:def_7;
now__::_thesis:_not_P19_meets_P29
assume P19 meets P29 ; ::_thesis: contradiction
then consider p0 being set such that
A34: p0 in P19 and
A35: p0 in P29 by XBOOLE_0:3;
A36: p0 in P1 by A34, XBOOLE_0:def_5;
A37: not p0 in {p1,p2} by A34, XBOOLE_0:def_5;
p0 in P2 by A35, XBOOLE_0:def_5;
hence contradiction by A9, A36, A37, XBOOLE_0:def_4; ::_thesis: verum
end;
hence not Q is connected by A13, A14, A15, A25, A33, TOPREAL5:1; ::_thesis: verum
end;
theorem Th48: :: JORDAN6:48
for P, P1, P2, P19, P29 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds
( P1 = P29 & P2 = P19 )
proof
let P, P1, P2, P19, P29 be Subset of the carrier of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds
( P1 = P29 & P2 = P19 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) implies ( P1 = P29 & P2 = P19 ) )
assume that
A1: P is being_simple_closed_curve and
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P1 \/ P2 = P and
A5: P19 is_an_arc_of p1,p2 and
A6: P29 is_an_arc_of p1,p2 and
A7: P19 \/ P29 = P ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
reconsider P = P as Simple_closed_curve by A1;
A8: p1 <> p2 by A6, Th37;
A9: p1 in P19 by A5, TOPREAL1:1;
A10: p2 in P19 by A5, TOPREAL1:1;
A11: p1 in P2 by A3, TOPREAL1:1;
A12: p2 in P2 by A3, TOPREAL1:1;
A13: p1 in P1 by A2, TOPREAL1:1;
A14: p2 in P1 by A2, TOPREAL1:1;
A15: P1 c= P by A4, XBOOLE_1:7;
A16: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider Q1 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A15, A16, XBOOLE_1:1;
A17: P2 c= P by A4, XBOOLE_1:7;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider Q2 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A17, XBOOLE_1:1;
A18: P19 c= P by A7, XBOOLE_1:7;
P19 \ {p1,p2} c= P19 by XBOOLE_1:36;
then reconsider Q19 = P19 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A18, XBOOLE_1:1;
A19: P29 c= P by A7, XBOOLE_1:7;
P29 \ {p1,p2} c= P29 by XBOOLE_1:36;
then reconsider Q29 = P29 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A19, XBOOLE_1:1;
A20: Q1 \/ Q2 = P \ {p1,p2} by A4, XBOOLE_1:42;
A21: Q19 \/ Q29 = P \ {p1,p2} by A7, XBOOLE_1:42;
then A22: Q19 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, XBOOLE_1:7, XBOOLE_1:12;
A23: Q29 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A24: Q1 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
A25: Q2 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12;
[#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5;
then reconsider R1 = Q1 as Subset of ((TOP-REAL 2) | P1) by XBOOLE_1:36;
R1 is connected by A2, Th40;
then A26: Q1 is connected by A4, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5;
then reconsider R2 = Q2 as Subset of ((TOP-REAL 2) | P2) by XBOOLE_1:36;
R2 is connected by A3, Th40;
then A27: Q2 is connected by A4, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P19) = P19 by PRE_TOPC:def_5;
then reconsider R19 = Q19 as Subset of ((TOP-REAL 2) | P19) by XBOOLE_1:36;
R19 is connected by A5, Th40;
then A28: Q19 is connected by A7, Th41, XBOOLE_1:7;
[#] ((TOP-REAL 2) | P29) = P29 by PRE_TOPC:def_5;
then reconsider R29 = Q29 as Subset of ((TOP-REAL 2) | P29) by XBOOLE_1:36;
R29 is connected by A6, Th40;
then A29: Q29 is connected by A7, Th41, XBOOLE_1:7;
A30: {p1,p2} c= P1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P1 )
assume x in {p1,p2} ; ::_thesis: x in P1
hence x in P1 by A13, A14, TARSKI:def_2; ::_thesis: verum
end;
A31: {p1,p2} c= P2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P2 )
assume x in {p1,p2} ; ::_thesis: x in P2
hence x in P2 by A11, A12, TARSKI:def_2; ::_thesis: verum
end;
A32: {p1,p2} c= P19
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P19 )
assume x in {p1,p2} ; ::_thesis: x in P19
hence x in P19 by A9, A10, TARSKI:def_2; ::_thesis: verum
end;
A33: {p1,p2} c= P29
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P29 )
assume x in {p1,p2} ; ::_thesis: x in P29
then ( x = p1 or x = p2 ) by TARSKI:def_2;
hence x in P29 by A6, TOPREAL1:1; ::_thesis: verum
end;
A34: Q1 \/ {p1,p2} = P1 by A30, XBOOLE_1:45;
A35: Q2 \/ {p1,p2} = P2 by A31, XBOOLE_1:45;
A36: Q19 \/ {p1,p2} = P19 by A32, XBOOLE_1:45;
A37: Q29 \/ {p1,p2} = P29 by A33, XBOOLE_1:45;
now__::_thesis:_(_(_not_P1_=_P29_or_not_P2_=_P19_)_&_not_(_P1_=_P19_&_P2_=_P29_)_implies_(_P1_=_P29_&_P2_=_P19_)_)
assume A38: ( not P1 = P29 or not P2 = P19 ) ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
now__::_thesis:_(_(_P1_<>_P29_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_P2_<>_P19_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_)
percases ( P1 <> P29 or P2 <> P19 ) by A38;
caseA39: P1 <> P29 ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
A40: now__::_thesis:_(_Q1_\_Q29_=_{}_implies_not_Q29_\_Q1_=_{}_)
assume that
A41: Q1 \ Q29 = {} and
A42: Q29 \ Q1 = {} ; ::_thesis: contradiction
A43: Q1 c= Q29 by A41, XBOOLE_1:37;
Q29 c= Q1 by A42, XBOOLE_1:37;
hence contradiction by A34, A37, A39, A43, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_(_Q1_\_Q29_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_Q29_\_Q1_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_)
percases ( Q1 \ Q29 <> {} or Q29 \ Q1 <> {} ) by A40;
caseA44: Q1 \ Q29 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
set y = the Element of Q1 \ Q29;
A45: the Element of Q1 \ Q29 in Q1 by A44, XBOOLE_0:def_5;
then A46: the Element of Q1 \ Q29 in Q19 \/ Q29 by A20, A21, XBOOLE_0:def_3;
not the Element of Q1 \ Q29 in Q29 by A44, XBOOLE_0:def_5;
then the Element of Q1 \ Q29 in Q19 by A46, XBOOLE_0:def_3;
then Q1 /\ Q19 <> {} by A45, XBOOLE_0:def_4;
then A47: Q1 meets Q19 by XBOOLE_0:def_7;
now__::_thesis:_not_Q2_meets_Q19
assume Q2 meets Q19 ; ::_thesis: contradiction
then (Q1 \/ Q19) \/ Q2 is connected by A26, A27, A28, A47, JORDAN1:4;
hence contradiction by A8, A13, A14, A15, A20, A22, Th47, XBOOLE_1:4; ::_thesis: verum
end;
then A48: Q2 /\ Q19 = {} by XBOOLE_0:def_7;
A49: Q2 c= Q29
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q2 or x in Q29 )
assume A50: x in Q2 ; ::_thesis: x in Q29
then x in Q1 \/ Q2 by XBOOLE_0:def_3;
then ( x in Q19 or x in Q29 ) by A20, A21, XBOOLE_0:def_3;
hence x in Q29 by A48, A50, XBOOLE_0:def_4; ::_thesis: verum
end;
Q19 c= Q1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q19 or x in Q1 )
assume A51: x in Q19 ; ::_thesis: x in Q1
then x in Q1 \/ Q2 by A20, A21, XBOOLE_0:def_3;
then ( x in Q1 or x in Q2 ) by XBOOLE_0:def_3;
hence x in Q1 by A48, A51, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A49, Th46, XBOOLE_1:9; ::_thesis: verum
end;
caseA52: Q29 \ Q1 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
set y = the Element of Q29 \ Q1;
A53: the Element of Q29 \ Q1 in Q29 by A52, XBOOLE_0:def_5;
then A54: the Element of Q29 \ Q1 in Q2 \/ Q1 by A20, A21, XBOOLE_0:def_3;
not the Element of Q29 \ Q1 in Q1 by A52, XBOOLE_0:def_5;
then the Element of Q29 \ Q1 in Q2 by A54, XBOOLE_0:def_3;
then Q29 /\ Q2 <> {} by A53, XBOOLE_0:def_4;
then A55: Q29 meets Q2 by XBOOLE_0:def_7;
now__::_thesis:_not_Q19_meets_Q2
assume Q19 meets Q2 ; ::_thesis: contradiction
then (Q29 \/ Q2) \/ Q19 is connected by A27, A28, A29, A55, JORDAN1:4;
hence contradiction by A8, A13, A14, A15, A21, A25, Th47, XBOOLE_1:4; ::_thesis: verum
end;
then A56: Q19 /\ Q2 = {} by XBOOLE_0:def_7;
A57: Q19 c= Q1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q19 or x in Q1 )
assume A58: x in Q19 ; ::_thesis: x in Q1
then x in Q19 \/ Q29 by XBOOLE_0:def_3;
then ( x in Q1 or x in Q2 ) by A20, A21, XBOOLE_0:def_3;
hence x in Q1 by A56, A58, XBOOLE_0:def_4; ::_thesis: verum
end;
Q2 c= Q29
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q2 or x in Q29 )
assume A59: x in Q2 ; ::_thesis: x in Q29
then x in Q2 \/ Q1 by XBOOLE_0:def_3;
then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def_3;
hence x in Q29 by A56, A59, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A57, Th46, XBOOLE_1:9; ::_thesis: verum
end;
end;
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum
end;
caseA60: P2 <> P19 ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
A61: now__::_thesis:_(_Q2_\_Q19_=_{}_implies_not_Q19_\_Q2_=_{}_)
assume that
A62: Q2 \ Q19 = {} and
A63: Q19 \ Q2 = {} ; ::_thesis: contradiction
A64: Q2 c= Q19 by A62, XBOOLE_1:37;
Q19 c= Q2 by A63, XBOOLE_1:37;
hence contradiction by A35, A36, A60, A64, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_(_Q2_\_Q19_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_Q19_\_Q2_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_)
percases ( Q2 \ Q19 <> {} or Q19 \ Q2 <> {} ) by A61;
caseA65: Q2 \ Q19 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
set y = the Element of Q2 \ Q19;
A66: the Element of Q2 \ Q19 in Q2 by A65, XBOOLE_0:def_5;
then A67: the Element of Q2 \ Q19 in Q29 \/ Q19 by A20, A21, XBOOLE_0:def_3;
not the Element of Q2 \ Q19 in Q19 by A65, XBOOLE_0:def_5;
then the Element of Q2 \ Q19 in Q29 by A67, XBOOLE_0:def_3;
then Q2 /\ Q29 <> {} by A66, XBOOLE_0:def_4;
then A68: Q2 meets Q29 by XBOOLE_0:def_7;
now__::_thesis:_not_Q1_meets_Q29
assume Q1 meets Q29 ; ::_thesis: contradiction
then (Q2 \/ Q29) \/ Q1 is connected by A26, A27, A29, A68, JORDAN1:4;
hence contradiction by A8, A13, A14, A15, A20, A23, Th47, XBOOLE_1:4; ::_thesis: verum
end;
then A69: Q1 /\ Q29 = {} by XBOOLE_0:def_7;
A70: Q1 c= Q19
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q1 or x in Q19 )
assume A71: x in Q1 ; ::_thesis: x in Q19
then x in Q2 \/ Q1 by XBOOLE_0:def_3;
then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def_3;
hence x in Q19 by A69, A71, XBOOLE_0:def_4; ::_thesis: verum
end;
Q29 c= Q2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q29 or x in Q2 )
assume A72: x in Q29 ; ::_thesis: x in Q2
then x in Q2 \/ Q1 by A20, A21, XBOOLE_0:def_3;
then ( x in Q2 or x in Q1 ) by XBOOLE_0:def_3;
hence x in Q2 by A69, A72, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A70, Th46, XBOOLE_1:9; ::_thesis: verum
end;
caseA73: Q19 \ Q2 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) )
set y = the Element of Q19 \ Q2;
A74: the Element of Q19 \ Q2 in Q19 by A73, XBOOLE_0:def_5;
then A75: the Element of Q19 \ Q2 in Q1 \/ Q2 by A20, A21, XBOOLE_0:def_3;
not the Element of Q19 \ Q2 in Q2 by A73, XBOOLE_0:def_5;
then the Element of Q19 \ Q2 in Q1 by A75, XBOOLE_0:def_3;
then Q19 /\ Q1 <> {} by A74, XBOOLE_0:def_4;
then A76: Q19 meets Q1 by XBOOLE_0:def_7;
now__::_thesis:_not_Q29_meets_Q1
assume Q29 meets Q1 ; ::_thesis: contradiction
then (Q19 \/ Q1) \/ Q29 is connected by A26, A28, A29, A76, JORDAN1:4;
hence contradiction by A8, A13, A14, A15, A21, A24, Th47, XBOOLE_1:4; ::_thesis: verum
end;
then A77: Q29 /\ Q1 = {} by XBOOLE_0:def_7;
A78: Q29 c= Q2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q29 or x in Q2 )
assume A79: x in Q29 ; ::_thesis: x in Q2
then x in Q29 \/ Q19 by XBOOLE_0:def_3;
then ( x in Q2 or x in Q1 ) by A20, A21, XBOOLE_0:def_3;
hence x in Q2 by A77, A79, XBOOLE_0:def_4; ::_thesis: verum
end;
Q1 c= Q19
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q1 or x in Q19 )
assume A80: x in Q1 ; ::_thesis: x in Q19
then x in Q19 \/ Q29 by A20, A21, XBOOLE_0:def_3;
then ( x in Q19 or x in Q29 ) by XBOOLE_0:def_3;
hence x in Q19 by A77, A80, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A78, Th46, XBOOLE_1:9; ::_thesis: verum
end;
end;
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum
end;
end;
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum
end;
hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum
end;
begin
Lm1: for g being Function of I[01],R^1
for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
proof
let g be Function of I[01],R^1; ::_thesis: for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
let s1, s2, r be real number ; ::_thesis: ( g is continuous & g . 0[01] < r & r < g . 1[01] implies ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) )
assume that
A1: g is continuous and
A2: g . 0[01] < r and
A3: r < g . 1[01] ; ::_thesis: ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
ex rc being Real st
( g . rc = r & 0 < rc & rc < 1 ) by A1, A2, A3, BORSUK_1:def_14, BORSUK_1:def_15, TOPMETR:20, TOPREAL5:6;
hence ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r ) ; ::_thesis: verum
end;
theorem Th49: :: JORDAN6:49
for P1 being Subset of (TOP-REAL 2)
for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
proof
let P1 be Subset of (TOP-REAL 2); ::_thesis: for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
let r be real number ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 implies ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) )
assume that
A1: p1 `1 <= r and
A2: r <= p2 `1 and
A3: P1 is_an_arc_of p1,p2 ; ::_thesis: ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )
reconsider P19 = P1 as non empty Subset of (TOP-REAL 2) by A3, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL 2) | P19) such that
A4: f is being_homeomorphism and
A5: f . 0 = p1 and
A6: f . 1 = p2 by A3, TOPREAL1:def_1;
A7: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5;
then reconsider f1 = f as Function of the carrier of I[01], the carrier of (TOP-REAL 2) by FUNCT_2:7;
reconsider f2 = f1 as Function of I[01],(TOP-REAL 2) ;
reconsider proj11 = proj1 as Function of the carrier of (TOP-REAL 2),REAL ;
reconsider proj12 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider g1 = proj11 * f1 as Function of the carrier of I[01],REAL ;
reconsider g = g1 as Function of I[01],R^1 by TOPMETR:17;
f is continuous by A4, TOPS_2:def_5;
then A8: f2 is continuous by Th3;
A9: proj12 is continuous by TOPREAL5:10;
A10: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1;
then A11: 0 in dom f by XXREAL_1:1;
A12: 1 in dom f by A10, XXREAL_1:1;
A13: g . 0 = proj1 . p1 by A5, A11, FUNCT_1:13
.= p1 `1 by PSCOMP_1:def_5 ;
A14: g . 1 = proj1 . p2 by A6, A12, FUNCT_1:13
.= p2 `1 by PSCOMP_1:def_5 ;
reconsider P19 = P19 as non empty Subset of (TOP-REAL 2) ;
A15: P19 is closed by A3, COMPTS_1:7, JORDAN5A:1;
A16: Vertical_Line r is closed by Th6;
now__::_thesis:_(_(_g_._0_=_g_._1_&_P1_meets_Vertical_Line_r_)_or_(_g_._0[01]_=_r_&_P1_meets_Vertical_Line_r_)_or_(_g_._1[01]_=_r_&_P1_meets_Vertical_Line_r_)_or_(_g_._0[01]_<_r_&_r_<_g_._1[01]_&_P1_meets_Vertical_Line_r_)_)
percases ( g . 0 = g . 1 or g . 0[01] = r or g . 1[01] = r or ( g . 0[01] < r & r < g . 1[01] ) ) by A1, A2, A13, A14, BORSUK_1:def_14, BORSUK_1:def_15, XXREAL_0:1;
case g . 0 = g . 1 ; ::_thesis: P1 meets Vertical_Line r
then A17: g . 0 = r by A1, A2, A13, A14, XXREAL_0:1;
A18: f . 0 in rng f by A11, FUNCT_1:def_3;
then f . 0 in P1 by A7;
then reconsider p = f . 0 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 0) by PSCOMP_1:def_5
.= r by A11, A17, FUNCT_1:13 ;
then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A7, A18, XBOOLE_0:3; ::_thesis: verum
end;
caseA19: g . 0[01] = r ; ::_thesis: P1 meets Vertical_Line r
A20: f . 0 in rng f by A11, FUNCT_1:def_3;
then f . 0 in P19 by A7;
then reconsider p = f . 0 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 0) by PSCOMP_1:def_5
.= r by A11, A19, BORSUK_1:def_14, FUNCT_1:13 ;
then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A7, A20, XBOOLE_0:3; ::_thesis: verum
end;
caseA21: g . 1[01] = r ; ::_thesis: P1 meets Vertical_Line r
A22: f . 1 in rng f by A12, FUNCT_1:def_3;
then f . 1 in P1 by A7;
then reconsider p = f . 1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . 1) by PSCOMP_1:def_5
.= r by A12, A21, BORSUK_1:def_15, FUNCT_1:13 ;
then f . 1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A7, A22, XBOOLE_0:3; ::_thesis: verum
end;
case ( g . 0[01] < r & r < g . 1[01] ) ; ::_thesis: P1 meets Vertical_Line r
then consider r1 being Real such that
A23: 0 < r1 and
A24: r1 < 1 and
A25: g . r1 = r by A8, A9, Lm1;
dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1;
then A26: r1 in dom f by A23, A24, XXREAL_1:1;
A27: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5;
A28: f . r1 in rng f by A26, FUNCT_1:def_3;
then f . r1 in P19 by A27;
then reconsider p = f . r1 as Point of (TOP-REAL 2) ;
p `1 = proj1 . (f . r1) by PSCOMP_1:def_5
.= r by A25, A26, FUNCT_1:13 ;
then f . r1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ;
hence P1 meets Vertical_Line r by A27, A28, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) by A15, A16, TOPS_1:8; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_P_being_Simple_closed_curve
for_P1,_P19_being_non_empty_Subset_of_(TOP-REAL_2)_st_ex_P2_being_non_empty_Subset_of_(TOP-REAL_2)_st_
(_P1_is_an_arc_of_W-min_P,_E-max_P_&_P2_is_an_arc_of_E-max_P,_W-min_P_&_P1_/\_P2_=_{(W-min_P),(E-max_P)}_&_P1_\/_P2_=_P_&_(First_Point_(P1,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P2,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_&_ex_P29_being_non_empty_Subset_of_(TOP-REAL_2)_st_
(_P19_is_an_arc_of_W-min_P,_E-max_P_&_P29_is_an_arc_of_E-max_P,_W-min_P_&_P19_/\_P29_=_{(W-min_P),(E-max_P)}_&_P19_\/_P29_=_P_&_(First_Point_(P19,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P29,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_holds_
P1_=_P19
let P be Simple_closed_curve; ::_thesis: for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds
P1 = P19
let P1, P19 be non empty Subset of (TOP-REAL 2); ::_thesis: ( ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) implies P1 = P19 )
assume that
A1: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) and
A2: ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ; ::_thesis: P1 = P19
consider P2 being non empty Subset of (TOP-REAL 2) such that
A3: P1 is_an_arc_of W-min P, E-max P and
A4: P2 is_an_arc_of E-max P, W-min P and
P1 /\ P2 = {(W-min P),(E-max P)} and
A5: P1 \/ P2 = P and
A6: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A1;
A7: P2 is_an_arc_of W-min P, E-max P by A4, JORDAN5B:14;
consider P29 being non empty Subset of (TOP-REAL 2) such that
A8: P19 is_an_arc_of W-min P, E-max P and
A9: P29 is_an_arc_of E-max P, W-min P and
P19 /\ P29 = {(W-min P),(E-max P)} and
A10: P19 \/ P29 = P and
A11: (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A2;
A12: P29 is_an_arc_of W-min P, E-max P by A9, JORDAN5B:14;
now__::_thesis:_(_P1_=_P29_implies_not_P2_=_P19_)
assume that
A13: P1 = P29 and
A14: P2 = P19 ; ::_thesis: contradiction
A15: (W-min P) `1 = W-bound P by EUCLID:52;
A16: (E-max P) `1 = E-bound P by EUCLID:52;
then A17: (W-min P) `1 < (E-max P) `1 by A15, TOPREAL5:17;
then A18: (W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 by A15, A16, XREAL_1:226;
A19: ((W-bound P) + (E-bound P)) / 2 <= (E-max P) `1 by A15, A16, A17, XREAL_1:226;
then A20: P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A7, A18, Th49;
P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A7, A18, A19, Th49;
then A21: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (First_Point (P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A4, A6, A20, JORDAN5C:18;
A22: P29 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A12, A18, A19, Th49;
P29 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, A18, A19, Th49;
hence contradiction by A9, A11, A13, A14, A21, A22, JORDAN5C:18; ::_thesis: verum
end;
hence P1 = P19 by A3, A5, A7, A8, A10, A12, Th48; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
assume A1: P is being_simple_closed_curve ;
func Upper_Arc P -> non empty Subset of (TOP-REAL 2) means :Def8: :: JORDAN6:def 8
( it is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & it /\ P2 = {(W-min P),(E-max P)} & it \/ P2 = P & (First_Point (it,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )
proof
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, Th33;
hence ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point (b2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds
b1 = b2 by A1, Lm2;
end;
:: deftheorem Def8 defines Upper_Arc JORDAN6:def_8_:_
for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Upper_Arc P iff ( b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point (b2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) );
definition
let P be Subset of (TOP-REAL 2);
assume A1: P is being_simple_closed_curve ;
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;
func Lower_Arc P -> non empty Subset of (TOP-REAL 2) means :Def9: :: JORDAN6:def 9
( it is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ it = {(W-min P),(E-max P)} & (Upper_Arc P) \/ it = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, Def8;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 holds
b1 = b2
proof
let P1, P19 be non empty Subset of (TOP-REAL 2); ::_thesis: ( P1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & P19 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P19 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P19 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P19,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 implies P1 = P19 )
assume that
A3: P1 is_an_arc_of E-max P, W-min P and
(Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and
A4: (Upper_Arc P) \/ P1 = P and
(First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 and
A5: P19 is_an_arc_of E-max P, W-min P and
(Upper_Arc P) /\ P19 = {(W-min P),(E-max P)} and
A6: (Upper_Arc P) \/ P19 = P and
(First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P19,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: P1 = P19
A7: P1 is_an_arc_of W-min P, E-max P by A3, JORDAN5B:14;
P19 is_an_arc_of W-min P, E-max P by A5, JORDAN5B:14;
then ( P1 = P19 or ( Upper_Arc P = P19 & P1 = Upper_Arc P ) ) by A1, A2, A4, A6, A7, Th48;
hence P1 = P19 ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Lower_Arc JORDAN6:def_9_:_
for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Lower_Arc P iff ( b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );
theorem Th50: :: JORDAN6:50
for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )
assume A1: P is being_simple_closed_curve ; ::_thesis: ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;
Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;
hence ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, A2, Def9, JORDAN5B:14; ::_thesis: verum
end;
theorem Th51: :: JORDAN6:51
for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) )
assume A1: P is being_simple_closed_curve ; ::_thesis: ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )
then A2: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by Def9;
set B = Upper_Arc P;
set A = Lower_Arc P;
A3: (((Upper_Arc P) \/ (Lower_Arc P)) \ (Upper_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) = ((Lower_Arc P) \ (Upper_Arc P)) \/ ((Lower_Arc P) /\ (Upper_Arc P)) by XBOOLE_1:40
.= Lower_Arc P by XBOOLE_1:51 ;
(((Upper_Arc P) \/ (Lower_Arc P)) \ (Lower_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) = ((Upper_Arc P) \ (Lower_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) by XBOOLE_1:40
.= Upper_Arc P by XBOOLE_1:51 ;
hence ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) by A1, A2, A3, Def9; ::_thesis: verum
end;
theorem :: JORDAN6:52
for P being Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds
P1 = Lower_Arc P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds
P1 = Lower_Arc P
let P1 be Subset of ((TOP-REAL 2) | P); ::_thesis: ( P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P implies P1 = Lower_Arc P )
assume that
A1: P is being_simple_closed_curve and
A2: (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and
A3: (Upper_Arc P) \/ P1 = P ; ::_thesis: P1 = Lower_Arc P
set B = Upper_Arc P;
(((Upper_Arc P) \/ P1) \ (Upper_Arc P)) \/ ((Upper_Arc P) /\ P1) = (P1 \ (Upper_Arc P)) \/ (P1 /\ (Upper_Arc P)) by XBOOLE_1:40
.= P1 by XBOOLE_1:51 ;
hence P1 = Lower_Arc P by A1, A2, A3, Th51; ::_thesis: verum
end;
theorem :: JORDAN6:53
for P being Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds
P1 = Upper_Arc P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds
P1 = Upper_Arc P
let P1 be Subset of ((TOP-REAL 2) | P); ::_thesis: ( P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P implies P1 = Upper_Arc P )
assume that
A1: P is being_simple_closed_curve and
A2: P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} and
A3: P1 \/ (Lower_Arc P) = P ; ::_thesis: P1 = Upper_Arc P
set B = Lower_Arc P;
((P1 \/ (Lower_Arc P)) \ (Lower_Arc P)) \/ (P1 /\ (Lower_Arc P)) = (P1 /\ (Lower_Arc P)) \/ (P1 \ (Lower_Arc P)) by XBOOLE_1:40
.= P1 by XBOOLE_1:51 ;
hence P1 = Upper_Arc P by A1, A2, A3, Th51; ::_thesis: verum
end;
begin
theorem Th54: :: JORDAN6:54
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds
q = p1
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds
q = p1
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 implies q = p1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q,p1,P,p1,p2 ; ::_thesis: q = p1
q in P by A2, JORDAN5C:def_3;
then LE p1,q,P,p1,p2 by A1, JORDAN5C:10;
hence q = p1 by A1, A2, JORDAN5C:12; ::_thesis: verum
end;
theorem Th55: :: JORDAN6:55
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds
q = p2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds
q = p2
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 implies q = p2 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE p2,q,P,p1,p2 ; ::_thesis: q = p2
q in P by A2, JORDAN5C:def_3;
then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;
hence q = p2 by A1, A2, JORDAN5C:12; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
let q1, q2 be Point of (TOP-REAL 2);
pred LE q1,q2,P means :Def10: :: JORDAN6:def 10
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) );
end;
:: deftheorem Def10 defines LE JORDAN6:def_10_:_
for P being Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) holds
( LE q1,q2,P iff ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) );
theorem :: JORDAN6:56
for P being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds
LE q,q,P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds
LE q,q,P
let q be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & q in P implies LE q,q,P )
assume that
A1: P is being_simple_closed_curve and
A2: q in P ; ::_thesis: LE q,q,P
A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, Def9;
A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;
now__::_thesis:_(_(_q_in_Upper_Arc_P_&_LE_q,q,P_)_or_(_q_in_Lower_Arc_P_&_not_q_in_Upper_Arc_P_&_LE_q,q,P_)_)
percases ( q in Upper_Arc P or ( q in Lower_Arc P & not q in Upper_Arc P ) ) by A2, A3, XBOOLE_0:def_3;
caseA5: q in Upper_Arc P ; ::_thesis: LE q,q,P
then LE q,q, Upper_Arc P, W-min P, E-max P by JORDAN5C:9;
hence LE q,q,P by A5, Def10; ::_thesis: verum
end;
caseA6: ( q in Lower_Arc P & not q in Upper_Arc P ) ; ::_thesis: LE q,q,P
then A7: LE q,q, Lower_Arc P, E-max P, W-min P by JORDAN5C:9;
q <> W-min P by A4, A6, TOPREAL1:1;
hence LE q,q,P by A6, A7, Def10; ::_thesis: verum
end;
end;
end;
hence LE q,q,P ; ::_thesis: verum
end;
theorem :: JORDAN6:57
for P being Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2
let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P implies q1 = q2 )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q1,P ; ::_thesis: q1 = q2
A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;
A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9;
A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;
now__::_thesis:_(_(_q1_in_Upper_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_q1_=_q2_)_or_(_q1_in_Upper_Arc_P_&_q2_in_Upper_Arc_P_&_LE_q1,q2,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q1_in_Lower_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q2,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_)
percases ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A2, Def10;
caseA7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; ::_thesis: q1 = q2
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_)
percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
caseA8: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2
then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4;
then A9: q1 = E-max P by A5, A8, TARSKI:def_2;
q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, A8, XBOOLE_0:def_4;
hence q1 = q2 by A5, A7, A9, TARSKI:def_2; ::_thesis: verum
end;
caseA10: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4;
then q2 = E-max P by A5, A7, TARSKI:def_2;
hence q1 = q2 by A6, A10, Th55; ::_thesis: verum
end;
caseA11: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2
then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4;
then q1 = E-max P by A5, A11, TARSKI:def_2;
hence q1 = q2 by A4, A11, Th54; ::_thesis: verum
end;
end;
end;
hence q1 = q2 ; ::_thesis: verum
end;
caseA12: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_)
percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
caseA13: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2
then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def_4;
then q1 = E-max P by A5, A13, TARSKI:def_2;
hence q1 = q2 by A6, A12, Th55; ::_thesis: verum
end;
case ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2
hence q1 = q2 by A6, A12, JORDAN5C:12; ::_thesis: verum
end;
caseA14: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2
then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def_4;
then q1 = E-max P by A5, A14, TARSKI:def_2;
hence q1 = q2 by A4, A14, Th54; ::_thesis: verum
end;
end;
end;
hence q1 = q2 ; ::_thesis: verum
end;
caseA15: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_)
percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
case ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def_4;
then q2 = E-max P by A5, A15, TARSKI:def_2;
hence q1 = q2 by A4, A15, Th54; ::_thesis: verum
end;
caseA16: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def_4;
then q2 = E-max P by A5, A15, TARSKI:def_2;
hence q1 = q2 by A6, A16, Th55; ::_thesis: verum
end;
case ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2
hence q1 = q2 by A4, A15, JORDAN5C:12; ::_thesis: verum
end;
end;
end;
hence q1 = q2 ; ::_thesis: verum
end;
end;
end;
hence q1 = q2 ; ::_thesis: verum
end;
theorem :: JORDAN6:58
for P being Subset of (TOP-REAL 2)
for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds
LE q1,q3,P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds
LE q1,q3,P
let q1, q2, q3 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P implies LE q1,q3,P )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P ; ::_thesis: LE q1,q3,P
A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;
A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9;
A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;
now__::_thesis:_(_(_q1_in_Upper_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q3,P_)_or_(_q1_in_Upper_Arc_P_&_q2_in_Upper_Arc_P_&_LE_q1,q2,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q1_in_Lower_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q2,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_)
percases ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A2, Def10;
caseA7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; ::_thesis: LE q1,q3,P
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_)
percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P
hence LE q1,q3,P by A7, Def10; ::_thesis: verum
end;
caseA8: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4;
then q2 = E-max P by A5, A7, TARSKI:def_2;
hence LE q1,q3,P by A2, A6, A8, Th55; ::_thesis: verum
end;
case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P
hence LE q1,q3,P by A7, Def10; ::_thesis: verum
end;
end;
end;
hence LE q1,q3,P ; ::_thesis: verum
end;
caseA9: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_)
percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P
hence LE q1,q3,P by A9, Def10; ::_thesis: verum
end;
caseA10: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P
then LE q1,q3, Upper_Arc P, W-min P, E-max P by A9, JORDAN5C:13;
hence LE q1,q3,P by A9, A10, Def10; ::_thesis: verum
end;
case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P
hence LE q1,q3,P by A9, Def10; ::_thesis: verum
end;
end;
end;
hence LE q1,q3,P ; ::_thesis: verum
end;
caseA11: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P
now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_)
percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10;
caseA12: ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A11, XBOOLE_0:def_4;
then q2 = E-max P by A5, A11, TARSKI:def_2;
then LE q2,q3, Lower_Arc P, E-max P, W-min P by A4, A12, JORDAN5C:10;
then LE q1,q3, Lower_Arc P, E-max P, W-min P by A11, JORDAN5C:13;
hence LE q1,q3,P by A11, A12, Def10; ::_thesis: verum
end;
caseA13: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P
then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A11, XBOOLE_0:def_4;
then q2 = E-max P by A5, A11, TARSKI:def_2;
hence LE q1,q3,P by A2, A6, A13, Th55; ::_thesis: verum
end;
caseA14: ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P
then LE q1,q3, Lower_Arc P, E-max P, W-min P by A11, JORDAN5C:13;
hence LE q1,q3,P by A11, A14, Def10; ::_thesis: verum
end;
end;
end;
hence LE q1,q3,P ; ::_thesis: verum
end;
end;
end;
hence LE q1,q3,P ; ::_thesis: verum
end;
theorem :: JORDAN6:59
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p2 holds
not p2 in L_Segment (P,p1,p2,q)
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p2 holds
not p2 in L_Segment (P,p1,p2,q)
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q <> p2 implies not p2 in L_Segment (P,p1,p2,q) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q <> p2 ; ::_thesis: not p2 in L_Segment (P,p1,p2,q)
assume p2 in L_Segment (P,p1,p2,q) ; ::_thesis: contradiction
then ex w being Point of (TOP-REAL 2) st
( p2 = w & LE w,q,P,p1,p2 ) ;
hence contradiction by A1, A2, Th55; ::_thesis: verum
end;
theorem :: JORDAN6:60
for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds
not p1 in R_Segment (P,p1,p2,q)
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds
not p1 in R_Segment (P,p1,p2,q)
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q <> p1 implies not p1 in R_Segment (P,p1,p2,q) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q <> p1 ; ::_thesis: not p1 in R_Segment (P,p1,p2,q)
assume p1 in R_Segment (P,p1,p2,q) ; ::_thesis: contradiction
then ex w being Point of (TOP-REAL 2) st
( p1 = w & LE q,w,P,p1,p2 ) ;
hence contradiction by A1, A2, Th54; ::_thesis: verum
end;
registration
let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2);
cluster Lower_Arc S -> non empty compact ;
coherence
( not Lower_Arc S is empty & Lower_Arc S is compact )
proof
Lower_Arc S is_an_arc_of E-max S, W-min S by Def9;
hence ( not Lower_Arc S is empty & Lower_Arc S is compact ) by JORDAN5A:1; ::_thesis: verum
end;
cluster Upper_Arc S -> non empty compact ;
coherence
( not Upper_Arc S is empty & Upper_Arc S is compact )
proof
Upper_Arc S is_an_arc_of W-min S, E-max S by Def8;
hence ( not Upper_Arc S is empty & Upper_Arc S is compact ) by JORDAN5A:1; ::_thesis: verum
end;
end;
theorem Th61: :: JORDAN6:61
for S being non empty being_simple_closed_curve Subset of (TOP-REAL 2) holds
( Lower_Arc S c= S & Upper_Arc S c= S )
proof
let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( Lower_Arc S c= S & Upper_Arc S c= S )
S = (Lower_Arc S) \/ (Upper_Arc S) by Th50;
hence ( Lower_Arc S c= S & Upper_Arc S c= S ) by XBOOLE_1:7; ::_thesis: verum
end;
definition
let C be Simple_closed_curve;
func Lower_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 11
First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
coherence
First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;
func Upper_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 12
First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
coherence
First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;
end;
:: deftheorem defines Lower_Middle_Point JORDAN6:def_11_:_
for C being Simple_closed_curve holds Lower_Middle_Point C = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
:: deftheorem defines Upper_Middle_Point JORDAN6:def_12_:_
for C being Simple_closed_curve holds Upper_Middle_Point C = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
theorem Th62: :: JORDAN6:62
for C being Simple_closed_curve holds Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
proof
let C be Simple_closed_curve; ::_thesis: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
A1: W-bound C <= E-bound C by SPRECT_1:21;
(W-min C) `1 = W-bound C by EUCLID:52;
then A2: (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, Th1;
(E-max C) `1 = E-bound C by EUCLID:52;
then A3: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, Th1;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
hence Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; ::_thesis: verum
end;
theorem Th63: :: JORDAN6:63
for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
proof
let C be Simple_closed_curve; ::_thesis: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
A1: W-bound C <= E-bound C by SPRECT_1:21;
(W-min C) `1 = W-bound C by EUCLID:52;
then A2: (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, Th1;
(E-max C) `1 = E-bound C by EUCLID:52;
then A3: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, Th1;
Upper_Arc C is_an_arc_of W-min C, E-max C by Th50;
hence Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; ::_thesis: verum
end;
theorem :: JORDAN6:64
for C being Simple_closed_curve holds (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let C be Simple_closed_curve; ::_thesis: (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th62;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6;
then A2: (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A1, A2, JORDAN5C:def_1;
then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by XBOOLE_0:def_4;
hence (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by Th31; ::_thesis: verum
end;
theorem :: JORDAN6:65
for C being Simple_closed_curve holds (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
proof
let C be Simple_closed_curve; ::_thesis: (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th63;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6;
then A2: (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
Upper_Arc C is_an_arc_of W-min C, E-max C by Th50;
then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A1, A2, JORDAN5C:def_1;
then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by XBOOLE_0:def_4;
hence (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by Th31; ::_thesis: verum
end;
theorem :: JORDAN6:66
for C being Simple_closed_curve holds Lower_Middle_Point C in Lower_Arc C
proof
let C be Simple_closed_curve; ::_thesis: Lower_Middle_Point C in Lower_Arc C
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th62;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6;
then A2: (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) /\ (Lower_Arc C) by A1, A2, JORDAN5C:def_1;
hence Lower_Middle_Point C in Lower_Arc C by XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th67: :: JORDAN6:67
for C being Simple_closed_curve holds Upper_Middle_Point C in Upper_Arc C
proof
let C be Simple_closed_curve; ::_thesis: Upper_Middle_Point C in Upper_Arc C
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th63;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6;
then A2: (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
A3: Upper_Arc C is_an_arc_of E-max C, W-min C by Th50;
then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) = Last_Point ((Upper_Arc C),(E-max C),(W-min C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A1, A2, JORDAN5C:18;
then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) /\ (Upper_Arc C) by A1, A2, A3, JORDAN5C:def_2;
hence Upper_Middle_Point C in Upper_Arc C by XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: JORDAN6:68
for C being Simple_closed_curve holds Upper_Middle_Point C in C
proof
let C be Simple_closed_curve; ::_thesis: Upper_Middle_Point C in C
A1: Upper_Middle_Point C in Upper_Arc C by Th67;
Upper_Arc C c= C by Th61;
hence Upper_Middle_Point C in C by A1; ::_thesis: verum
end;
theorem :: JORDAN6:69
for C being Simple_closed_curve
for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C
proof
let C be Simple_closed_curve; ::_thesis: for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C
let r be real number ; ::_thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C )
A1: (W-min C) `1 = W-bound C by EUCLID:52;
A2: (E-max C) `1 = E-bound C by EUCLID:52;
assume that
A3: W-bound C <= r and
A4: r <= E-bound C ; ::_thesis: LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C
Upper_Arc C is_an_arc_of W-min C, E-max C by Def8;
then Upper_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49;
then consider x being set such that
A5: x in (Upper_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;
A6: x in Upper_Arc C by A5, XBOOLE_0:def_4;
A7: x in Vertical_Line r by A5, XBOOLE_0:def_4;
reconsider fs = x as Point of (TOP-REAL 2) by A5;
A8: Upper_Arc C c= C by Th61;
then A9: S-bound C <= fs `2 by A6, PSCOMP_1:24;
A10: fs `2 <= N-bound C by A6, A8, PSCOMP_1:24;
A11: |[r,(S-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A12: |[r,(N-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A13: |[r,(S-bound C)]| `2 = S-bound C by EUCLID:52;
|[r,(N-bound C)]| `2 = N-bound C by EUCLID:52;
then x in LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) by A9, A10, A11, A12, A13, GOBOARD7:7;
hence LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C by A6, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: JORDAN6:70
for C being Simple_closed_curve
for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
proof
let C be Simple_closed_curve; ::_thesis: for r being real number st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
let r be real number ; ::_thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C )
A1: (W-min C) `1 = W-bound C by EUCLID:52;
A2: (E-max C) `1 = E-bound C by EUCLID:52;
assume that
A3: W-bound C <= r and
A4: r <= E-bound C ; ::_thesis: LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
Lower_Arc C is_an_arc_of E-max C, W-min C by Def9;
then Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN5B:14;
then Lower_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49;
then consider x being set such that
A5: x in (Lower_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;
A6: x in Lower_Arc C by A5, XBOOLE_0:def_4;
A7: x in Vertical_Line r by A5, XBOOLE_0:def_4;
reconsider fs = x as Point of (TOP-REAL 2) by A5;
A8: Lower_Arc C c= C by Th61;
then A9: S-bound C <= fs `2 by A6, PSCOMP_1:24;
A10: fs `2 <= N-bound C by A6, A8, PSCOMP_1:24;
A11: |[r,(S-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A12: |[r,(N-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A13: |[r,(S-bound C)]| `2 = S-bound C by EUCLID:52;
|[r,(N-bound C)]| `2 = N-bound C by EUCLID:52;
then x in LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) by A9, A10, A11, A12, A13, GOBOARD7:7;
hence LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C by A6, XBOOLE_0:3; ::_thesis: verum
end;