let C be Simple_closed_curve; :: thesis: for p, q being Point of st LE p,q,C & LE q, E-max C,C & p <> q holds
Segment p,q,C = Segment (Upper_Arc C),(W-min C),(E-max C),p,q
let p, q be Point of ; :: thesis: ( LE p,q,C & LE q, E-max C,C & p <> q implies Segment p,q,C = Segment (Upper_Arc C),(W-min C),(E-max C),p,q )
assume that
A1: LE p,q,C and
A2: LE q, E-max C,C and
A3: p <> q ; :: thesis: Segment p,q,C = Segment (Upper_Arc C),(W-min C),(E-max C),p,q
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:65;
A5: LE p, E-max C,C by A1, A2, JORDAN6:73;
A6: p in Upper_Arc C by A1, A2, JORDAN17:3, JORDAN6:73;
A7: q in Upper_Arc C by A2, JORDAN17:3;
A8: Upper_Arc C c= C by JORDAN6:76;

A9: now

assume q = W-min C ; :: thesis: contradiction
then LE q,p,C by A6, A8, JORDAN7:3;
hence contradiction by A1, A3, JORDAN6:72; :: thesis: verum

end;

defpred S₁[ Point of ] means ( LE p,$1,C & LE $1,q,C );
defpred S₂[ Point of ] means ( LE p,$1, Upper_Arc C, W-min C, E-max C & LE $1,q, Upper_Arc C, W-min C, E-max C );
A10: for p1 being Point of holds
( S₁[p1] iff S₂[p1] )

proof

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

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

assume that
A11: LE p,p1,C and
A12: LE p1,q,C ; :: thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C & LE p1,q, Upper_Arc C, W-min C, E-max C )

hereby :: thesis: LE p1,q, Upper_Arc C, W-min C, E-max C

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

suppose p1 = E-max C ; :: thesis: LE p,p1, Upper_Arc C, W-min C, E-max C

hence LE p,p1, Upper_Arc C, W-min C, E-max C by A4, A6, JORDAN5C:10; :: thesis: verum

end;

suppose p1 = W-min C ; :: thesis: LE p,p1, Upper_Arc C, W-min C, E-max C

then LE p1,p,C by A6, A8, JORDAN7:3;
then p = p1 by A11, JORDAN6:72;
hence LE p,p1, Upper_Arc C, W-min C, E-max C by A5, JORDAN17:3, JORDAN5C:9; :: thesis: verum

end;

suppose that A13: p1 <> E-max C and
A14: p1 <> W-min C ; :: thesis: LE p,p1, Upper_Arc C, W-min C, E-max C

now

assume A15: p1 in Lower_Arc C ; :: thesis: contradiction
p1 in Upper_Arc C by A2, A12, JORDAN17:3, JORDAN6:73;
then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A15, XBOOLE_0:def 4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:65;
hence contradiction by A13, A14, TARSKI:def 2; :: thesis: verum

end;

hence LE p,p1, Upper_Arc C, W-min C, E-max C by A11, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

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

suppose A16: q = E-max C ; :: thesis: LE p1,q, Upper_Arc C, W-min C, E-max C

then p1 in Upper_Arc C by A12, JORDAN17:3;
hence LE p1,q, Upper_Arc C, W-min C, E-max C by A4, A16, JORDAN5C:10; :: thesis: verum

end;

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

now

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

end;

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

end;

end;

end;

assume that
A18: LE p,p1, Upper_Arc C, W-min C, E-max C and
A19: LE p1,q, Upper_Arc C, W-min C, E-max C ; :: thesis: S₁[p1]
A20: p1 in Upper_Arc C by A18, JORDAN5C:def 3;
hence LE p,p1,C by A6, A18, JORDAN6:def 10; :: thesis: LE p1,q,C
thus LE p1,q,C by A7, A19, A20, JORDAN6:def 10; :: thesis: verum

end;

deffunc H₁( set ) -> set = $1;
set X = { H₁(p1) where p1 is Point of : S₁[p1] } ;
set Y = { H₁(p1) where p1 is Point of : S₂[p1] } ;
A21: { H₁(p1) where p1 is Point of : S₁[p1] } = { H₁(p1) where p1 is Point of : S₂[p1] } from FRAENKEL:sch 3(A10);
Segment p,q,C = { H₁(p1) where p1 is Point of : S₁[p1] } by A9, JORDAN7:def 1;
hence Segment p,q,C = Segment (Upper_Arc C),(W-min C),(E-max C),p,q by A21, JORDAN6:29; :: thesis: verum