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

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