let C be Simple_closed_curve; :: thesis: for p, q being Point of () st LE p, E-max C,C & LE E-max C,q,C holds
Segment (p,q,C) = (R_Segment ((),(),(),p)) \/ (L_Segment ((),(),(),q))

let p, q be Point of (); :: thesis: ( LE p, E-max C,C & LE E-max C,q,C implies Segment (p,q,C) = (R_Segment ((),(),(),p)) \/ (L_Segment ((),(),(),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 ((),(),(),p)) \/ (L_Segment ((),(),(),q))
A3: p in Upper_Arc C by ;
A4: q in Lower_Arc C by ;
A5: now :: thesis: not q = W-min Cend;
A6: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
defpred S1[ Point of ()] means ( LE p,\$1,C & LE \$1,q,C );
defpred S2[ Point of ()] means LE p,\$1, Upper_Arc C, W-min C, E-max C;
defpred S3[ Point of ()] means LE \$1,q, Lower_Arc C, E-max C, W-min C;
defpred S4[ Point of ()] means ( S2[\$1] or S3[\$1] );
A7: for p1 being Point of () holds
( S1[p1] iff S4[p1] )
proof
let p1 be Point of (); :: thesis: ( 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 ) :: thesis: ( S4[p1] implies S1[p1] )
proof
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 )
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 () /\ () by ;
then p1 in {(),()} by JORDAN6:def 9;
hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def 2; :: thesis: verum
end;
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 ; :: 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 ;
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 ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
suppose not p1 in Lower_Arc 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 ; :: thesis: verum
end;
suppose not p1 in Upper_Arc 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 ; :: thesis: 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 ) ; :: thesis: 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 ; :: thesis: S1[p1]
then A16: p1 in Upper_Arc C by JORDAN5C:def 3;
hence LE p,p1,C by ; :: thesis: LE p1,q,C
thus LE p1,q,C by ; :: thesis: verum
end;
suppose that A17: LE p1,q, Lower_Arc C, E-max C, W-min C and
A18: p1 <> W-min C ; :: thesis: S1[p1]
A19: p1 in Lower_Arc C by ;
hence LE p,p1,C by ; :: thesis: LE p1,q,C
thus LE p1,q,C by ; :: thesis: verum
end;
end;
end;
set Y1 = { p1 where p1 is Point of () : S2[p1] } ;
set Y2 = { p1 where p1 is Point of () : S3[p1] } ;
deffunc H1( set ) -> set = \$1;
set X = { H1(p1) where p1 is Point of () : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of () : S4[p1] } ;
set Y9 = { p1 where p1 is Point of () : ( S2[p1] or S3[p1] ) } ;
A20: { H1(p1) where p1 is Point of () : S1[p1] } = { H1(p1) where p1 is Point of () : S4[p1] } from A21: Segment (p,q,C) = { H1(p1) where p1 is Point of () : S1[p1] } by ;
A22: L_Segment ((),(),(),q) = { p1 where p1 is Point of () : S3[p1] } by JORDAN6:def 3;
{ p1 where p1 is Point of () : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of () : S2[p1] } \/ { p1 where p1 is Point of () : S3[p1] } from hence Segment (p,q,C) = (R_Segment ((),(),(),p)) \/ (L_Segment ((),(),(),q)) by ; :: thesis: verum