let C be Simple_closed_curve; 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); ( 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
; 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;
defpred S1[ Point of (TOP-REAL 2)] means ( LE E-max C,$1,C & LE $1,q,C );
defpred S2[ 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
( S1[p1] iff S2[p1] )
proof
let p1 be
Point of
(TOP-REAL 2);
( S1[p1] iff S2[p1] )
hereby ( S2[p1] implies S1[p1] )
assume that A9:
LE E-max C,
p1,
C
and A10:
LE p1,
q,
C
;
( 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;
LE p1,q, Lower_Arc C, E-max C, W-min C
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
;
S1[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;
LE p1,q,C
thus
LE p1,
q,
C
by A4, A6, A17, A18, JORDAN6:def 10;
verum
end;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
A19:
{ H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] }
from FRAENKEL:sch 3(A8);
Segment ((E-max C),q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[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; verum