let C be Simple_closed_curve; for a, b, c, d being Point of (TOP-REAL 2) st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds
a,d,c,b are_in_this_order_on C
let a, b, c, d be Point of (TOP-REAL 2); ( a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C implies a,d,c,b are_in_this_order_on C )
assume that
A1:
a in C
and
A2:
b in C
and
A3:
c in C
and
A4:
d in C
; ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
per cases
( ( LE a,b,C & LE b,c,C & LE c,d,C ) or ( LE a,b,C & LE b,c,C & not LE c,d,C ) or ( LE a,b,C & not LE b,c,C & LE c,d,C ) or ( LE a,b,C & not LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & LE b,c,C & LE c,d,C ) or ( not LE a,b,C & LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & not LE c,d,C ) )
;
suppose
(
LE a,
b,
C &
LE b,
c,
C &
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
;
verum end; suppose A5:
(
LE a,
b,
C &
LE b,
c,
C & not
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A6:
LE d,
c,
C
by A3, A4, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,d,C or LE d,a,C )
by A1, A4, JORDAN16:7;
suppose A7:
LE a,
d,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE b,
d,
C or
LE d,
b,
C )
by A2, A4, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A5, A6, A7;
verum end; suppose
LE d,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A5;
verum end; end;
end; end; suppose A8:
(
LE a,
b,
C & not
LE b,
c,
C &
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A9:
LE c,
b,
C
by A2, A3, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE b,d,C or LE d,b,C )
by A2, A4, JORDAN16:7;
suppose A10:
LE b,
d,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE a,
c,
C or
LE c,
a,
C )
by A1, A3, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A8, A9, A10;
verum end; suppose A11:
LE d,
b,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,c,C or LE c,a,C )
by A1, A3, JORDAN16:7;
suppose
LE a,
c,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A8, A11;
verum end; suppose A12:
LE c,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE a,
d,
C or
LE d,
a,
C )
by A1, A4, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A8, A11, A12;
verum end; end;
end; end; end;
end; end; suppose A13:
(
LE a,
b,
C & not
LE b,
c,
C & not
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A14:
LE d,
c,
C
by A3, A4, JORDAN16:7;
A15:
LE c,
b,
C
by A2, A3, A13, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,c,C or LE c,a,C )
by A1, A3, JORDAN16:7;
suppose A16:
LE a,
c,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE a,
d,
C or
LE d,
a,
C )
by A1, A4, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A15, A14, A16;
verum end; suppose
LE c,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A13, A14;
verum end; end;
end; end; suppose A17:
( not
LE a,
b,
C &
LE b,
c,
C &
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A18:
LE b,
a,
C
by A1, A2, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,d,C or LE d,a,C )
by A1, A4, JORDAN16:7;
suppose A19:
LE a,
d,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE a,
c,
C or
LE c,
a,
C )
by A1, A3, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A17, A18, A19;
verum end; suppose
LE d,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A17;
verum end; end;
end; end; suppose A20:
( not
LE a,
b,
C &
LE b,
c,
C & not
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A21:
(
LE b,
a,
C &
LE d,
c,
C )
by A1, A2, A3, A4, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,d,C or LE d,a,C )
by A1, A4, JORDAN16:7;
suppose
LE a,
d,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A21;
verum end; suppose A22:
LE d,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )A23:
(
LE b,
d,
C or
LE d,
b,
C )
by A2, A4, JORDAN16:7;
(
LE a,
c,
C or
LE c,
a,
C )
by A1, A3, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A20, A21, A22, A23;
verum end; end;
end; end; suppose A24:
( not
LE a,
b,
C & not
LE b,
c,
C &
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A25:
(
LE b,
a,
C &
LE c,
b,
C )
by A1, A2, A3, JORDAN16:7;
thus
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
verumproof
per cases
( LE a,d,C or LE d,a,C )
by A1, A4, JORDAN16:7;
suppose
LE a,
d,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A25;
verum end; suppose A26:
LE d,
a,
C
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )
(
LE b,
d,
C or
LE d,
b,
C )
by A2, A4, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A24, A25, A26;
verum end; end;
end; end; suppose A27:
( not
LE a,
b,
C & not
LE b,
c,
C & not
LE c,
d,
C )
;
( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )then A28:
LE d,
c,
C
by A3, A4, JORDAN16:7;
(
LE b,
a,
C &
LE c,
b,
C )
by A1, A2, A3, A27, JORDAN16:7;
hence
(
a,
b,
c,
d are_in_this_order_on C or
a,
b,
d,
c are_in_this_order_on C or
a,
c,
b,
d are_in_this_order_on C or
a,
c,
d,
b are_in_this_order_on C or
a,
d,
b,
c are_in_this_order_on C or
a,
d,
c,
b are_in_this_order_on C )
by A28;
verum end; end;