let C be Simple_closed_curve; for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
let p, q be Point of (TOP-REAL 2); ( LE p, E-max C,C & LE E-max C,q,C implies Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) )
assume that
A1:
LE p, E-max C,C
and
A2:
LE E-max C,q,C
; Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
A3:
p in Upper_Arc C
by A1, JORDAN17:3;
A4:
q in Lower_Arc C
by A2, JORDAN17:4;
A6:
Lower_Arc C is_an_arc_of E-max C, W-min C
by JORDAN6:50;
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, Upper_Arc C, W-min C, E-max C;
defpred S3[ Point of (TOP-REAL 2)] means LE $1,q, Lower_Arc C, E-max C, W-min C;
defpred S4[ Point of (TOP-REAL 2)] means ( S2[$1] or S3[$1] );
A7:
for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S4[p1] )
proof
let p1 be
Point of
(TOP-REAL 2);
( S1[p1] iff S4[p1] )
thus
(
LE p,
p1,
C &
LE p1,
q,
C & not
LE p,
p1,
Upper_Arc C,
W-min C,
E-max C implies
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C )
( S4[p1] implies S1[p1] )proof
assume that A8:
LE p,
p1,
C
and A9:
LE p1,
q,
C
;
( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
per cases
( p1 = W-min C or p1 = E-max C or not p1 in Lower_Arc C or not p1 in Upper_Arc C )
by A10;
suppose A13:
p1 = W-min C
;
( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )then
p = W-min C
by A8, JORDAN7:2;
hence
(
LE p,
p1,
Upper_Arc C,
W-min C,
E-max C or
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C )
by A1, A13, JORDAN17:3, JORDAN5C:9;
verum end; suppose
p1 = E-max C
;
( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )hence
(
LE p,
p1,
Upper_Arc C,
W-min C,
E-max C or
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C )
by A4, A6, JORDAN5C:10;
verum end; end;
end;
assume A14:
(
LE p,
p1,
Upper_Arc C,
W-min C,
E-max C or
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C )
;
S1[p1]
per cases
( LE p,p1, Upper_Arc C, W-min C, E-max C or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 <> W-min C ) or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) )
by A14;
suppose A15:
LE p,
p1,
Upper_Arc C,
W-min C,
E-max C
;
S1[p1]then A16:
p1 in Upper_Arc C
by JORDAN5C:def 3;
hence
LE p,
p1,
C
by A3, A15, JORDAN6:def 10;
LE p1,q,Cthus
LE p1,
q,
C
by A4, A5, A16, JORDAN6:def 10;
verum end; suppose that A17:
LE p1,
q,
Lower_Arc C,
E-max C,
W-min C
and A18:
p1 <> W-min C
;
S1[p1]A19:
p1 in Lower_Arc C
by A17, JORDAN5C:def 3;
hence
LE p,
p1,
C
by A3, A18, JORDAN6:def 10;
LE p1,q,Cthus
LE p1,
q,
C
by A4, A5, A17, A19, JORDAN6:def 10;
verum end; end;
end;
set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } ;
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) : S4[p1] } ;
set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } ;
A20:
{ H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] }
from FRAENKEL:sch 3(A7);
A21:
Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] }
by A5, JORDAN7:def 1;
A22:
L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] }
by JORDAN6:def 3;
{ p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] }
from TOPREAL1:sch 1();
hence
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
by A20, A21, A22, JORDAN6:def 4; verum