let P be Subset of (TOP-REAL 2); 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); ( 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
; 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 ( ( 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 ) )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 A2;
case A7:
(
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P )
;
LE q1,q3,Pnow ( ( 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
;
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 )
;
LE q1,q3,Pnow ( ( 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
;
verum end; 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 )
;
LE q1,q3,Pnow ( ( 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;
case A11:
(
q2 in Upper_Arc P &
q3 in Lower_Arc P & not
q3 = W-min P )
;
LE q1,q3,Pthen
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;
verum end; end; end; hence
LE q1,
q3,
P
;
verum end; end; end;
hence
LE q1,q3,P
; verum