let P be Simple_closed_curve; :: thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P holds
a = d
let a, b, c, d be Point of (TOP-REAL 2); :: thesis: ( a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P implies a = d )
assume that
A1: a <> b and
A2: a <> c and
A3: b <> d and
A4: a,b,c,d are_in_this_order_on P and
A5: d,b,c,a are_in_this_order_on P ; :: thesis: a = d
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 = d
then A7: LE a,c,P by JORDAN6:58;
thus a = d :: thesis: verum
proof
per cases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5;
suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; :: thesis: a = d
hence a = d by A2, A7, JORDAN6:57; :: thesis: verum
end;
suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; :: thesis: a = d
hence a = d by A2, A7, JORDAN6:57; :: thesis: verum
end;
suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; :: thesis: a = d
hence a = d by A2, A7, JORDAN6:57; :: thesis: verum
end;
suppose A8: ( LE a,d,P & LE d,b,P & LE b,c,P ) ; :: thesis: a = d
LE b,d,P by A6, JORDAN6:58;
hence a = d by A3, A8, JORDAN6:57; :: thesis: verum
end;
end;
end;
end;
suppose A9: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; :: thesis: a = d
then A10: LE b,d,P by JORDAN6:58;
thus a = d :: thesis: verum
proof
per cases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5;
suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; :: thesis: a = d
hence a = d by A3, A10, JORDAN6:57; :: thesis: verum
end;
suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; :: thesis: a = d
hence a = d by A9, JORDAN6:57; :: thesis: verum
end;
suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; :: thesis: a = d
hence a = d by A9, JORDAN6:57; :: thesis: verum
end;
suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; :: thesis: a = d
hence a = d by A9, JORDAN6:57; :: thesis: verum
end;
end;
end;
end;
suppose A11: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; :: thesis: a = d
thus a = d :: thesis: verum
proof
per cases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5;
suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; :: thesis: a = d
then LE b,a,P by JORDAN6:58;
hence a = d by A1, A11, JORDAN6:57; :: thesis: verum
end;
suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; :: thesis: a = d
hence a = d by A11, JORDAN6:57; :: thesis: verum
end;
suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; :: thesis: a = d
hence a = d by A11, JORDAN6:57; :: thesis: verum
end;
suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; :: thesis: a = d
hence a = d by A11, JORDAN6:57; :: thesis: verum
end;
end;
end;
end;
suppose A12: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; :: thesis: a = d
thus a = d :: thesis: verum
proof
per cases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5;
suppose A13: ( LE d,b,P & LE b,c,P & LE c,a,P ) ; :: thesis: a = d
LE a,c,P by A12, JORDAN6:58;
hence a = d by A2, A13, JORDAN6:57; :: thesis: verum
end;
suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; :: thesis: a = d
hence a = d by A12, JORDAN6:57; :: thesis: verum
end;
suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; :: thesis: a = d
hence a = d by A12, JORDAN6:57; :: thesis: verum
end;
suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; :: thesis: a = d
hence a = d by A12, JORDAN6:57; :: thesis: verum
end;
end;
end;
end;
end;