let C be Simple_closed_curve; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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;

defpred S_{1}[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C );

defpred S_{2}[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C;

defpred S_{3}[ Point of (TOP-REAL 2)] means LE $1,q, Lower_Arc C, E-max C, W-min C;

defpred S_{4}[ Point of (TOP-REAL 2)] means ( S_{2}[$1] or S_{3}[$1] );

A7: for p1 being Point of (TOP-REAL 2) holds

( S_{1}[p1] iff S_{4}[p1] )
_{2}[p1] } ;

set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S_{3}[p1] } ;

deffunc H_{1}( set ) -> set = $1;

set X = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[p1] } ;

set Y = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{4}[p1] } ;

set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S_{2}[p1] or S_{3}[p1] ) } ;

A20: { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[p1] } = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{4}[p1] }
from FRAENKEL:sch 3(A7);

A21: Segment (p,q,C) = { H_{1}(p1) where p1 is Point of (TOP-REAL 2) : S_{1}[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) : S_{3}[p1] }
by JORDAN6:def 3;

{ p1 where p1 is Point of (TOP-REAL 2) : ( S_{2}[p1] or S_{3}[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S_{2}[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S_{3}[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; :: thesis: verum

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); :: thesis: ( 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 ; :: thesis: 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;

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

A6:
Lower_Arc C is_an_arc_of E-max C, W-min C
by JORDAN6:50;assume
q = W-min C
; :: thesis: contradiction

then W-min C = E-max C by A2, JORDAN7:2;

hence contradiction by TOPREAL5:19; :: thesis: verum

end;then W-min C = E-max C by A2, JORDAN7:2;

hence contradiction by TOPREAL5:19; :: thesis: verum

defpred S

defpred S

defpred S

defpred S

A7: for p1 being Point of (TOP-REAL 2) holds

( S

proof

set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S
let p1 be Point of (TOP-REAL 2); :: thesis: ( S_{1}[p1] iff S_{4}[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 ) :: thesis: ( S_{4}[p1] implies S_{1}[p1] )_{1}[p1]

end;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 ) :: thesis: ( S

proof

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 )
; :: thesis: S
assume that

A8: LE p,p1,C and

A9: LE p1,q,C ; :: thesis: ( 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 )

end;A8: LE p,p1,C and

A9: LE p1,q,C ; :: thesis: ( 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 )

A10: now :: thesis: ( p1 in Lower_Arc C & p1 in Upper_Arc C & not p1 = W-min C implies p1 = E-max C )

assume that

A11: p1 in Lower_Arc C and

A12: p1 in Upper_Arc C ; :: thesis: ( p1 = W-min C or p1 = E-max C )

p1 in (Lower_Arc C) /\ (Upper_Arc C) by A11, A12, XBOOLE_0:def 4;

then p1 in {(W-min C),(E-max C)} by JORDAN6:def 9;

hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def 2; :: thesis: verum

end;A11: p1 in Lower_Arc C and

A12: p1 in Upper_Arc C ; :: thesis: ( p1 = W-min C or p1 = E-max C )

p1 in (Lower_Arc C) /\ (Upper_Arc C) by A11, A12, XBOOLE_0:def 4;

then p1 in {(W-min C),(E-max C)} by JORDAN6:def 9;

hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def 2; :: thesis: verum

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;

end;

suppose A13:
p1 = W-min C
; :: thesis: ( 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; :: thesis: verum

end;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; :: thesis: verum

suppose
p1 = E-max C
; :: thesis: ( 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; :: thesis: verum

end;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;

end;

suppose A15:
LE p,p1, Upper_Arc C, W-min C, E-max C
; :: thesis: S_{1}[p1]

then A16:
p1 in Upper_Arc C
by JORDAN5C:def 3;

hence LE p,p1,C by A3, A15, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A4, A5, A16, JORDAN6:def 10; :: thesis: verum

end;hence LE p,p1,C by A3, A15, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A4, A5, A16, JORDAN6:def 10; :: thesis: verum

suppose that A17:
LE p1,q, Lower_Arc C, E-max C, W-min C
and

A18: p1 <> W-min C ; :: thesis: S_{1}[p1]

A18: p1 <> W-min C ; :: thesis: S

A19:
p1 in Lower_Arc C
by A17, JORDAN5C:def 3;

hence LE p,p1,C by A3, A18, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A4, A5, A17, A19, JORDAN6:def 10; :: thesis: verum

end;hence LE p,p1,C by A3, A18, JORDAN6:def 10; :: thesis: LE p1,q,C

thus LE p1,q,C by A4, A5, A17, A19, JORDAN6:def 10; :: thesis: verum

set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S

deffunc H

set X = { H

set Y = { H

set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S

A20: { H

A21: Segment (p,q,C) = { H

A22: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = { p1 where p1 is Point of (TOP-REAL 2) : S

{ p1 where p1 is Point of (TOP-REAL 2) : ( S

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; :: thesis: verum