let P be Subset of (TOP-REAL 2); :: thesis: for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P implies q1 = q2 )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P ) ; :: thesis: q1 = q2
then A2: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by Def9;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th65;

now

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 A1, Def10;

case A4: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; :: thesis: q1 = q2

now

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 A1, Def10;

case A5: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A4, XBOOLE_0:def 4;
then A6: q1 = E-max P by A2, A5, TARSKI:def 2;
q2 in (Upper_Arc P) /\ (Lower_Arc P) by A4, A5, XBOOLE_0:def 4;
hence q1 = q2 by A2, A4, A6, TARSKI:def 2; :: thesis: verum

end;

case A7: ( 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 (Upper_Arc P) /\ (Lower_Arc P) by A4, XBOOLE_0:def 4;
then q2 = E-max P by A2, A4, TARSKI:def 2;
hence q1 = q2 by A3, A7, Th70; :: thesis: verum

end;

case A8: ( 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 (Upper_Arc P) /\ (Lower_Arc P) by A4, XBOOLE_0:def 4;
then q1 = E-max P by A2, A8, TARSKI:def 2;
hence q1 = q2 by A2, A8, Th69; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum

end;

case A9: ( 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

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 A1, Def10;

case A10: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A9, XBOOLE_0:def 4;
then q1 = E-max P by A2, A10, TARSKI:def 2;
hence q1 = q2 by A3, A9, Th70; :: 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 A3, A9, JORDAN5C:12; :: 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 (Upper_Arc P) /\ (Lower_Arc P) by A9, XBOOLE_0:def 4;
then q1 = E-max P by A2, A11, TARSKI:def 2;
hence q1 = q2 by A2, A11, Th69; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum

end;

case A12: ( 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

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 A1, Def10;

case ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis: q1 = q2

then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def 4;
then q2 = E-max P by A2, A12, TARSKI:def 2;
hence q1 = q2 by A2, A12, Th69; :: thesis: verum

end;

case A13: ( 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 (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def 4;
then q2 = E-max P by A2, A12, TARSKI:def 2;
hence q1 = q2 by A3, A13, Th70; :: 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 A2, A12, JORDAN5C:12; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum