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