let C be Simple_closed_curve; for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds
Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
let p, q be Point of (TOP-REAL 2); ( LE p,q,C & LE E-max C,p,C implies Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) )
assume that
A1:
LE p,q,C
and
A2:
LE E-max C,p,C
; Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
per cases
( p = E-max C or p <> E-max C )
;
suppose A3:
p <> E-max C
;
Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)A4:
Lower_Arc C is_an_arc_of E-max C,
W-min C
by JORDAN6:50;
A5:
q in Lower_Arc C
by A1, A2, JORDAN17:4, JORDAN6:58;
A6:
p in Lower_Arc C
by A2, JORDAN17:4;
A7:
Lower_Arc C c= C
by JORDAN6:61;
defpred S1[
Point of
(TOP-REAL 2)]
means (
LE p,$1,
C &
LE $1,
q,
C );
defpred S2[
Point of
(TOP-REAL 2)]
means (
LE p,$1,
Lower_Arc C,
E-max C,
W-min C &
LE $1,
q,
Lower_Arc C,
E-max C,
W-min C );
A12:
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 A13:
LE p,
p1,
C
and A14:
LE p1,
q,
C
;
( LE p,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C )hence
LE p,
p1,
Lower_Arc C,
E-max C,
W-min C
by A13, JORDAN6:def 10;
LE p1,q, Lower_Arc C, E-max C, W-min CA19:
p1 in Lower_Arc C
by A13, A17, JORDAN6:def 10;
end;
assume that A21:
LE p,
p1,
Lower_Arc C,
E-max C,
W-min C
and A22:
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C
;
S1[p1]
A23:
p1 <> W-min C
by A4, A10, A22, JORDAN6:55;
A24:
p1 in Lower_Arc C
by A21, JORDAN5C:def 3;
hence
LE p,
p1,
C
by A6, A21, A23, JORDAN6:def 10;
LE p1,q,C
thus
LE p1,
q,
C
by A5, A10, A22, A24, 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] } ;
A25:
{ 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(A12);
Segment (
p,
q,
C)
= { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] }
by A10, JORDAN7:def 1;
hence
Segment (
p,
q,
C)
= Segment (
(Lower_Arc C),
(E-max C),
(W-min C),
p,
q)
by A25, JORDAN6:26;
verum end; end;