let P be Subset of (TOP-REAL 2); :: thesis: for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds
LE q1,q3,P
let q1, q2, q3 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P implies LE q1,q3,P )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P ) ; :: thesis: LE q1,q3,P
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: LE q1,q3,P
now
per cases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A1, Def10;
case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; :: thesis: LE q1,q3,P
hence LE q1,q3,P by A4, Def10; :: thesis: verum
end;
case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; :: thesis: LE q1,q3,P
hence LE q1,q3,P by A4, Def10; :: thesis: verum
end;
end;
end;
hence LE q1,q3,P ; :: thesis: verum
end;
case A6: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; :: thesis: LE q1,q3,P
now
per cases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A1, Def10;
case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; :: thesis: LE q1,q3,P
hence LE q1,q3,P by A6, Def10; :: thesis: verum
end;
case A7: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; :: thesis: LE q1,q3,P
then LE q1,q3, Upper_Arc P, W-min P, E-max P by A6, JORDAN5C:13;
hence LE q1,q3,P by A6, A7, Def10; :: thesis: verum
end;
case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; :: thesis: LE q1,q3,P
hence LE q1,q3,P by A6, Def10; :: thesis: verum
end;
end;
end;
hence LE q1,q3,P ; :: thesis: verum
end;
case A8: ( 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: LE q1,q3,P
now
per cases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A1, Def10;
case A11: ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; :: thesis: LE q1,q3,P
then LE q1,q3, Lower_Arc P, E-max P, W-min P by A8, JORDAN5C:13;
hence LE q1,q3,P by A8, A11, Def10; :: thesis: verum
end;
end;
end;
hence LE q1,q3,P ; :: thesis: verum
end;
end;
end;
hence LE q1,q3,P ; :: thesis: verum