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