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 that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P and

A3: LE q2,q3,P ; :: thesis: LE q1,q3,P

A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;

A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9;

A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;

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 that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P and

A3: LE q2,q3,P ; :: thesis: LE q1,q3,P

A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;

A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9;

A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;

now :: thesis: ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q3,P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P & LE q1,q3,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 & LE q1,q3,P ) )end;

hence
LE q1,q3,P
; :: thesis: verumper 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;

end;

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

end;

now :: thesis: ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q1,q3,P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P & LE q1,q3,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 & LE q1,q3,P ) )end;

hence
LE q1,q3,P
; :: thesis: verumper 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 A3;

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: LE q1,q3,P

end;

now :: thesis: ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q1,q3,P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P & LE q1,q3,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 & LE q1,q3,P ) )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 A3;

end;

hence
LE q1,q3,P
; :: thesis: verumend;

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

end;

now :: thesis: ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q1,q3,P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P & LE q1,q3,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 & LE q1,q3,P ) )end;

hence
LE q1,q3,P
; :: thesis: verumper 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 A3;

end;

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

then
q2 in (Upper_Arc P) /\ (Lower_Arc P)
by A10, XBOOLE_0:def 4;

then q2 = E-max P by A5, A10, TARSKI:def 2;

then LE q2,q3, Lower_Arc P, E-max P, W-min P by A4, A11, JORDAN5C:10;

then LE q1,q3, Lower_Arc P, E-max P, W-min P by A10, JORDAN5C:13;

hence LE q1,q3,P by A11; :: thesis: verum

end;then q2 = E-max P by A5, A10, TARSKI:def 2;

then LE q2,q3, Lower_Arc P, E-max P, W-min P by A4, A11, JORDAN5C:10;

then LE q1,q3, Lower_Arc P, E-max P, W-min P by A10, JORDAN5C:13;

hence LE q1,q3,P by A11; :: thesis: verum