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