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

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