let P be Subset of (TOP-REAL 2); ( 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
; ( 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; verum