let P be Simple_closed_curve; :: thesis: for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
let b, c, a, d be Point of (TOP-REAL 2); :: thesis: ( b <> c & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) )
assume that
A1:
b <> c
and
A2:
( ( 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 ) )
; :: according to JORDAN17:def 1 :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
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 A2;
suppose A3:
(
LE a,
b,
P &
LE b,
c,
P &
LE c,
d,
P )
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )then consider e being
Point of
(TOP-REAL 2) such that A4:
(
e <> b &
e <> c &
LE b,
e,
P &
LE e,
c,
P )
by A1, Th8;
take
e
;
:: thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P )thus
(
e <> b &
e <> c &
a,
b,
e,
c are_in_this_order_on P )
by A3, A4, Def1;
:: thesis: verum end; suppose that A5:
LE b,
c,
P
and A6:
LE c,
d,
P
and A7:
LE d,
a,
P
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )consider e being
Point of
(TOP-REAL 2) such that A8:
(
e <> b &
e <> c &
LE b,
e,
P &
LE e,
c,
P )
by A1, A5, Th8;
take
e
;
:: thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
LE c,
a,
P
by A6, A7, JORDAN6:73;
hence
(
e <> b &
e <> c &
a,
b,
e,
c are_in_this_order_on P )
by A8, Def1;
:: thesis: verum end; suppose that A9:
LE c,
d,
P
and A10:
LE d,
a,
P
and A11:
LE a,
b,
P
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )thus
ex
e being
Point of
(TOP-REAL 2) st
(
e <> b &
e <> c &
a,
b,
e,
c are_in_this_order_on P )
:: thesis: verumproof
A12:
LE c,
a,
P
by A9, A10, JORDAN6:73;
per cases
( c = W-min P or c <> W-min P )
;
suppose A13:
c = W-min P
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
b in P
by A11, JORDAN7:5;
then consider e being
Point of
(TOP-REAL 2) such that A14:
e <> b
and A15:
LE b,
e,
P
by Th7;
take
e
;
:: thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P )thus
e <> b
by A14;
:: thesis: ( e <> c & a,b,e,c are_in_this_order_on P )thus
e <> c
by A1, A13, A15, JORDAN7:2;
:: thesis: a,b,e,c are_in_this_order_on Pthus
a,
b,
e,
c are_in_this_order_on P
by A11, A12, A15, Def1;
:: thesis: verum end; suppose A16:
c <> W-min P
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )take e =
W-min P;
:: thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
c in P
by A9, JORDAN7:5;
then A17:
LE e,
c,
P
by JORDAN7:3;
now assume A18:
e = b
;
:: thesis: contradiction
LE c,
a,
P
by A9, A10, JORDAN6:73;
then
LE c,
b,
P
by A11, JORDAN6:73;
hence
contradiction
by A1, A17, A18, JORDAN6:72;
:: thesis: verum end; hence
e <> b
;
:: thesis: ( e <> c & a,b,e,c are_in_this_order_on P )thus
e <> c
by A16;
:: thesis: a,b,e,c are_in_this_order_on Pthus
a,
b,
e,
c are_in_this_order_on P
by A11, A12, A17, Def1;
:: thesis: verum end;
end; end; suppose that
LE d,
a,
P
and A19:
(
LE a,
b,
P &
LE b,
c,
P )
;
:: thesis: ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )consider e being
Point of
(TOP-REAL 2) such that A20:
(
e <> b &
e <> c &
LE b,
e,
P &
LE e,
c,
P )
by A1, A19, Th8;
take
e
;
:: thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P )thus
(
e <> b &
e <> c &
a,
b,
e,
c are_in_this_order_on P )
by A19, A20, Def1;
:: thesis: verum end;