let P be Subset of (); :: thesis: for q1, q2 being Point of () st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2

let q1, q2 be Point of (); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P implies q1 = q2 )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q1,P ; :: thesis: q1 = q2
A4: Lower_Arc P is_an_arc_of E-max P, W-min P by ;
A5: (Upper_Arc P) /\ () = {(),()} by ;
A6: Upper_Arc P is_an_arc_of W-min P, E-max P by ;
now :: thesis: ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P & q1 = q2 ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P & q1 = q2 ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P & q1 = q2 ) )
per cases ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A2;
case A7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; :: thesis: q1 = q2
now :: thesis: ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P & q1 = q2 ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P & q1 = q2 ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P & q1 = q2 ) )
per cases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3;
case A8: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2
then q1 in () /\ () by ;
then A9: q1 = E-max P by ;
q2 in () /\ () by ;
hence q1 = q2 by ; :: thesis: verum
end;
case A10: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis: q1 = q2
then q2 in () /\ () by ;
then q2 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
case A11: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis: q1 = q2
then q1 in () /\ () by ;
then q1 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
end;
end;
hence q1 = q2 ; :: thesis: verum
end;
case A12: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; :: thesis: q1 = q2
now :: thesis: ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P & q1 = q2 ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P & q1 = q2 ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P & q1 = q2 ) )
per cases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3;
case A13: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2
then q1 in () /\ () by ;
then q1 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
case ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis: q1 = q2
hence q1 = q2 by ; :: thesis: verum
end;
case A14: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis: q1 = q2
then q1 in () /\ () by ;
then q1 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
end;
end;
hence q1 = q2 ; :: thesis: verum
end;
case A15: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; :: thesis: q1 = q2
now :: thesis: ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P & q1 = q2 ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P & q1 = q2 ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P & q1 = q2 ) )
per cases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3;
case ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2
then q2 in () /\ () by ;
then q2 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
case A16: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis: q1 = q2
then q2 in () /\ () by ;
then q2 = E-max P by ;
hence q1 = q2 by ; :: thesis: verum
end;
case ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis: q1 = q2
hence q1 = q2 by ; :: thesis: verum
end;
end;
end;
hence q1 = q2 ; :: thesis: verum
end;
end;
end;
hence q1 = q2 ; :: thesis: verum