let P be Subset of (TOP-REAL 2); :: thesis: for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds
P1 = Lower_Arc P
let P1 be Subset of ((TOP-REAL 2) | P); :: thesis: ( P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P implies P1 = Lower_Arc P )
assume that
A1: P is being_simple_closed_curve and
A2: (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and
A3: (Upper_Arc P) \/ P1 = P ; :: thesis: P1 = Lower_Arc P
set B = Upper_Arc P;
(((Upper_Arc P) \/ P1) \ (Upper_Arc P)) \/ ((Upper_Arc P) /\ P1) = (P1 \ (Upper_Arc P)) \/ (P1 /\ (Upper_Arc P)) by XBOOLE_1:40
.= P1 by XBOOLE_1:51 ;
hence P1 = Lower_Arc P by A1, A2, A3, Th51; :: thesis: verum