let P be Subset of (TOP-REAL 2); ( 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
; 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)
;
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)
;
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
;
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;
verum end; suppose A21:
(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 )now ( ( (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 ) )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 A21, XXREAL_0:1;
case A22:
(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 )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;
verum end; case A24:
(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
;
contradictionset 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;
verum 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
;
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
;
( 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;
verum