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