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