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 & E-max P in P )
by SPRECT_1:15, SPRECT_1:16;
W-min P <> E-max P
by TOPREAL5:25;
then consider P01, P02 being non empty Subset of (TOP-REAL 2) such that
A2:
( P01 is_an_arc_of W-min P, E-max P & P02 is_an_arc_of W-min P, E-max P & P = P01 \/ P02 & P01 /\ P02 = {(W-min P),(E-max P)} )
by A1, TOPREAL2:5;
reconsider P01 = P01, P02 = P02 as non empty Subset of (TOP-REAL 2) ;
A3:
P01 is_an_arc_of E-max P, W-min P
by A2, JORDAN5B:14;
A4:
P02 is_an_arc_of E-max P, W-min P
by A2, JORDAN5B:14;
reconsider P001 = P01, P002 = P02 as non empty Subset of (TOP-REAL 2) ;
A5:
(E-max P) `1 = E-bound P
by EUCLID:56;
A6:
Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed
by Th7;
P01 is closed
by A2, COMPTS_1:16, JORDAN5A:1;
then A7:
P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed
by A6, TOPS_1:35;
A8:
Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed
by Th7;
P02 is closed
by A2, COMPTS_1:16, JORDAN5A:1;
then A9:
P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed
by A8, TOPS_1:35;
consider q1 being Point of (TOP-REAL 2) such that
A10:
( q1 in P001 & q1 `1 = (((W-min P) `1 ) + ((E-max P) `1 )) / 2 )
by A2, Th13;
A11:
(W-min P) `1 = W-bound P
by EUCLID:56;
(E-max P) `1 = E-bound P
by EUCLID:56;
then
q1 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 }
by A10, A11;
then
P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {}
by A10, XBOOLE_0:def 4;
then A12:
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
A13:
( q2 in P002 & q2 `1 = (((W-min P) `1 ) + ((E-max P) `1 )) / 2 )
by A2, Th13;
q2 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 }
by A5, A11, A13;
then
P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {}
by A13, XBOOLE_0:def 4;
then A14:
P02 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2)
by XBOOLE_0:def 7;
per cases
( (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 A2, A4;
:: thesis: verum end; suppose A15:
(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 per cases
( (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 A15, XXREAL_0:1;
case A16:
(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 )A17:
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 A2, A7, A12, 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 A2, A9, A14, 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 A2, A3, A16, A17;
:: thesis: verum end; case A18:
(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: contradictionset p =
First_Point P01,
(W-min P),
(E-max P),
(Vertical_Line (((W-bound P) + (E-bound P)) / 2));
set p' =
Last_Point P02,
(E-max P),
(W-min P),
(Vertical_Line (((W-bound P) + (E-bound P)) / 2));
A19:
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 A2, A7, A12, JORDAN5C:def 1;
then A20:
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 A19, XBOOLE_0:def 4;
then A21:
(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 Th34;
A22:
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 A4, A9, A14, JORDAN5C:def 2;
then A23:
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 A22, 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 Th34;
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 A18, A21, TOPREAL3:11;
then
First_Point P01,
(W-min P),
(E-max P),
(Vertical_Line (((W-bound P) + (E-bound P)) / 2)) in P01 /\ P02
by A20, A23, 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 A2, TARSKI:def 2;
hence
contradiction
by A5, A11, A21, TOPREAL5:23;
:: thesis: verum end; then consider P1,
P2 being non
empty Subset of
(TOP-REAL 2) such that A24:
(
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 )
;
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 A24;
:: thesis: verum