let C be Simple_closed_curve; :: thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))
let q be Point of (TOP-REAL 2); :: thesis: ( LE E-max C,q,C implies Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) )
set p = W-min C;
assume A1: LE E-max C,q,C ; :: thesis: Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))
A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A3: W-min 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;
defpred S₁[ Point of (TOP-REAL 2)] means ( LE q,$1,C or ( q in C & $1 = W-min C ) );
defpred S₂[ Point of (TOP-REAL 2)] means ( LE q,$1, Lower_Arc C, E-max C, W-min C & LE $1, W-min C, Lower_Arc C, E-max C, W-min C );
A6: 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 A7: ( LE q,p1,C or ( q in C & p1 = W-min C ) ) ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

per cases ( ( q = E-max C & LE q,p1,C ) or ( q <> E-max C & LE q,p1,C ) or ( q in C & p1 = W-min C ) ) by A7;

suppose that A8: q = E-max C and
A9: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

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

end;

suppose that A11: q <> E-max C and
A12: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

A13: p1 in Lower_Arc C by A1, A12, JORDAN17:4, JORDAN6:58;

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

assume A15: q = W-min C ; :: thesis: contradiction
then LE q, E-max C,C by JORDAN7:3, SPRECT_1:14;
hence contradiction by A1, A15, JORDAN6:57, TOPREAL5:19; :: thesis: verum

end;

now :: thesis: not q in Upper_Arc C

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

end;

hence LE q,p1, Lower_Arc C, E-max C, W-min C by A12, JORDAN6:def 10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A13, JORDAN5C:10; :: thesis: verum

end;

suppose that q in C and
A16: p1 = W-min C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )

thus LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A4, A16, JORDAN5C:10; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A3, A16, JORDAN5C:9; :: thesis: verum

end;

end;

end;

assume that
A17: LE q,p1, Lower_Arc C, E-max C, W-min C and
LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; :: thesis: S₁[p1]
A18: p1 in Lower_Arc C by A17, JORDAN5C:def 3;
A19: q in Lower_Arc C by A17, JORDAN5C:def 3;

per cases ( p1 <> W-min C or p1 = W-min C ) ;

suppose p1 <> W-min C ; :: thesis: S₁[p1]

hence S₁[p1] by A17, A18, A19, JORDAN6:def 10; :: thesis: verum

end;

suppose p1 = W-min C ; :: thesis: S₁[p1]

hence S₁[p1] by A4, A5; :: thesis: verum

end;

end;

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] } ;
A20: { 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(A6);
Segment (q,(W-min C),C) = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } by JORDAN7:def 1;
hence Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) by A20, JORDAN6:26; :: thesis: verum