let P be Simple_closed_curve; for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P holds
c = d
let a, b, c, d be Point of (TOP-REAL 2); ( a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P implies c = d )
assume that
A1:
a <> b
and
A2:
a <> c
and
A3:
b <> d
and
A4:
a,b,c,d are_in_this_order_on P
and
A5:
a,b,d,c are_in_this_order_on P
; c = d
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 A4;
suppose A6:
(
LE a,
b,
P &
LE b,
c,
P &
LE c,
d,
P )
;
c = dthus
c = d
verumproof
per cases
( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) )
by A5;
end;
end; end; suppose A8:
(
LE b,
c,
P &
LE c,
d,
P &
LE d,
a,
P )
;
c = dthen A9:
LE c,
a,
P
by JORDAN6:58;
thus
c = d
verumproof
per cases
( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) )
by A5;
end;
end; end; suppose A11:
(
LE c,
d,
P &
LE d,
a,
P &
LE a,
b,
P )
;
c = dthen A12:
LE d,
b,
P
by JORDAN6:58;
thus
c = d
verumproof
per cases
( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) )
by A5;
end;
end; end; suppose A13:
(
LE d,
a,
P &
LE a,
b,
P &
LE b,
c,
P )
;
c = dthen A14:
LE d,
b,
P
by JORDAN6:58;
thus
c = d
verumproof
per cases
( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) )
by A5;
end;
end; end; end;