let C be Simple_closed_curve; :: thesis: for q being Point of () st LE E-max C,q,C holds
Segment (q,(),C) = Segment ((),(),(),q,())

let q be Point of (); :: thesis: ( LE E-max C,q,C implies Segment (q,(),C) = Segment ((),(),(),q,()) )
set p = W-min C;
assume A1: LE E-max C,q,C ; :: thesis: Segment (q,(),C) = Segment ((),(),(),q,())
A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A3: W-min C in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by ;
A5: Lower_Arc C c= C by JORDAN6:61;
defpred S1[ Point of ()] means ( LE q,\$1,C or ( q in C & \$1 = W-min C ) );
defpred S2[ Point of ()] means ( LE q,\$1, Lower_Arc C, E-max C, W-min C & LE \$1, W-min C, Lower_Arc C, E-max C, W-min C );
A6: for p1 being Point of () holds
( S1[p1] iff S2[p1] )
proof
let p1 be Point of (); :: thesis: ( S1[p1] iff S2[p1] )
hereby :: thesis: ( S2[p1] implies S1[p1] )
assume A7: ( LE q,p1,C or ( q in C & p1 = W-min C ) ) ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
per cases ( ( q = E-max C & LE q,p1,C ) or ( q <> E-max C & LE q,p1,C ) or ( q in C & p1 = W-min C ) ) by A7;
suppose that A8: q = E-max C and
A9: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A10: p1 in Lower_Arc C by ;
hence LE q,p1, Lower_Arc C, E-max C, W-min C by ; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by ; :: thesis: verum
end;
suppose that A11: q <> E-max C and
A12: LE q,p1,C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A13: p1 in Lower_Arc C by ;
A14: now :: thesis: not q = W-min Cend;
hence LE q,p1, Lower_Arc C, E-max C, W-min C by ; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by ; :: thesis: verum
end;
suppose that q in C and
A16: p1 = W-min C ; :: thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
thus LE q,p1, Lower_Arc C, E-max C, W-min C by ; :: thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by ; :: thesis: verum
end;
end;
end;
assume that
A17: LE q,p1, Lower_Arc C, E-max C, W-min C and
LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; :: thesis: S1[p1]
A18: p1 in Lower_Arc C by ;
A19: q in Lower_Arc C by ;
per cases ( p1 <> W-min C or p1 = W-min C ) ;
end;
end;
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 () : S2[p1] } ;
A20: { H1(p1) where p1 is Point of () : S1[p1] } = { H1(p1) where p1 is Point of () : S2[p1] } from Segment (q,(),C) = { H1(p1) where p1 is Point of () : S1[p1] } by JORDAN7:def 1;
hence Segment (q,(),C) = Segment ((),(),(),q,()) by ; :: thesis: verum