let C be Simple_closed_curve; :: thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)
let q be Point of (TOP-REAL 2); :: thesis: ( LE E-max C,q,C implies Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) )
set p = E-max C;
assume A1: LE E-max C,q,C ; :: thesis: Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)
A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A3: E-max C in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1, JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;

A6: now :: thesis: not q = W-min C

assume A7: q = W-min C ; :: thesis: contradiction
then E-max C = q by A1, JORDAN7:2;
hence contradiction by A7, TOPREAL5:19; :: thesis: verum

end;

defpred S₁[ Point of (TOP-REAL 2)] means ( LE E-max C,$1,C & LE $1,q,C );
defpred S₂[ Point of (TOP-REAL 2)] means ( LE E-max C,$1, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C );
A8: for p1 being Point of (TOP-REAL 2) holds
( S₁[p1] iff S₂[p1] )

proof

let p1 be Point of (TOP-REAL 2); :: thesis: ( S₁[p1] iff S₂[p1] )

hereby :: thesis: ( S₂[p1] implies S₁[p1] )

assume that
A9: LE E-max C,p1,C and
A10: LE p1,q,C ; :: thesis: ( LE E-max C,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C )
A11: p1 in Lower_Arc C by A9, JORDAN17:4;
hence LE E-max C,p1, Lower_Arc C, E-max C, W-min C by A2, JORDAN5C:10; :: thesis: LE p1,q, Lower_Arc C, E-max C, W-min C

per cases ( p1 = E-max C or p1 <> E-max C ) ;

suppose A12: p1 = E-max C ; :: thesis: LE p1,q, Lower_Arc C, E-max C, W-min C

then q in Lower_Arc C by A10, JORDAN17:4;
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A2, A12, JORDAN5C:10; :: thesis: verum

end;

suppose A13: p1 <> E-max C ; :: thesis: LE p1,q, Lower_Arc C, E-max C, W-min C

A14: now :: thesis: not p1 = W-min C

assume A15: p1 = W-min C ; :: thesis: contradiction
then LE p1, E-max C,C by A3, A5, JORDAN7:3;
hence contradiction by A9, A15, JORDAN6:57, TOPREAL5:19; :: thesis: verum

end;

now :: thesis: not p1 in Upper_Arc C

assume p1 in Upper_Arc C ; :: thesis: contradiction
then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A11, XBOOLE_0:def 4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A13, A14, TARSKI:def 2; :: thesis: verum

end;

hence LE p1,q, Lower_Arc C, E-max C, W-min C by A10, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

assume that
A16: LE E-max C,p1, Lower_Arc C, E-max C, W-min C and
A17: LE p1,q, Lower_Arc C, E-max C, W-min C ; :: thesis: S₁[p1]
A18: p1 in Lower_Arc C by A16, JORDAN5C:def 3;
p1 <> W-min C by A2, A6, A17, JORDAN6:55;
hence LE E-max C,p1,C by A3, A16, A18, JORDAN6:def 10; :: thesis: LE p1,q,C
thus LE p1,q,C by A4, A6, A17, A18, JORDAN6:def 10; :: thesis: verum

end;

deffunc H₁( set ) -> set = $1;
set X = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } ;
set Y = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₂[p1] } ;
A19: { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₂[p1] } from FRAENKEL:sch 3(A8);
Segment ((E-max C),q,C) = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } by A6, JORDAN7:def 1;
hence Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by A19, JORDAN6:26; :: thesis: verum