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

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