let P be Simple_closed_curve; :: thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P holds
a = c
let a, b, c, d be Point of (TOP-REAL 2); :: thesis: ( a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P implies a = c )
assume that
A1: a <> b and
A2: b <> c and
A3: c <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: c,b,a,d are_in_this_order_on P ; :: thesis: a = c

per cases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4;

suppose A6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; :: thesis: a = c

thus a = c :: thesis: verum

proof

per cases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5;

suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; :: thesis: a = c

hence a = c by A1, A6, JORDAN6:57; :: thesis: verum

end;

suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; :: thesis: a = c

hence a = c by A3, A6, JORDAN6:57; :: thesis: verum

end;

suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; :: thesis: a = c

hence a = c by A3, A6, JORDAN6:57; :: thesis: verum

end;

suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; :: thesis: a = c

hence a = c by A3, A6, JORDAN6:57; :: thesis: verum

end;

end;

end;

end;

suppose A7: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; :: thesis: a = c

thus a = c :: thesis: verum

proof

per cases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5;

suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; :: thesis: a = c

hence a = c by A2, A7, JORDAN6:57; :: thesis: verum

end;

suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; :: thesis: a = c

hence a = c by A3, A7, JORDAN6:57; :: thesis: verum

end;

suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; :: thesis: a = c

hence a = c by A3, A7, JORDAN6:57; :: thesis: verum

end;

suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; :: thesis: a = c

hence a = c by A3, A7, JORDAN6:57; :: thesis: verum

end;

end;

end;

end;

suppose A8: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; :: thesis: a = c

thus a = c :: thesis: verum

proof

per cases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5;

suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; :: thesis: a = c

hence a = c by A1, A8, JORDAN6:57; :: thesis: verum

end;

suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; :: thesis: a = c

hence a = c by A3, A8, JORDAN6:57; :: thesis: verum

end;

suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; :: thesis: a = c

hence a = c by A3, A8, JORDAN6:57; :: thesis: verum

end;

suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; :: thesis: a = c

hence a = c by A3, A8, JORDAN6:57; :: thesis: verum

end;

end;

end;

end;

suppose A9: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; :: thesis: a = c

thus a = c :: thesis: verum

proof

per cases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5;

suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; :: thesis: a = c

hence a = c by A2, A9, JORDAN6:57; :: thesis: verum

end;

suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; :: thesis: a = c

hence a = c by A1, A9, JORDAN6:57; :: thesis: verum

end;

suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; :: thesis: a = c

hence a = c by A2, A9, JORDAN6:57; :: thesis: verum

end;

suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; :: thesis: a = c

hence a = c by A1, A9, JORDAN6:57; :: thesis: verum

end;

end;

end;

end;

end;