let OAS be OAffinSpace; for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & o,a // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )
let o, a, b, a9, b9 be Element of OAS; ( not LIN o,a,b & o,a // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 implies ( o,b // o,b9 & a,b // a9,b9 ) )
assume that
A1:
not LIN o,a,b
and
A2:
o,a // o,a9
and
A3:
LIN o,b,b9
and
A4:
a,b '||' a9,b9
; ( o,b // o,b9 & a,b // a9,b9 )
A5:
o <> a
by A1, DIRAF:37;
consider a2 being Element of OAS such that
A6:
Mid a,o,a2
and
A7:
o <> a2
by DIRAF:17;
a,o // o,a2
by A6, DIRAF:def 3;
then consider b2 being Element of OAS such that
A8:
b,o // o,b2
and
A9:
b,a // a2,b2
by A5, ANALOAF:def 5;
A10:
o,b // b2,o
by A8, DIRAF:5;
a,o // o,a2
by A6, DIRAF:def 3;
then
a2,o // o,a
by DIRAF:5;
then A11:
a2,o // o,a9
by A2, A5, DIRAF:6;
LIN a,o,a2
by A6, DIRAF:34;
then A12:
LIN o,a2,a
by DIRAF:36;
A13:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
a2 // a,
b
by A9, DIRAF:5;
then
o,
a2 '||' a,
b
by DIRAF:def 4;
then
(
LIN o,
a2,
o &
LIN o,
a2,
b )
by A7, A12, DIRAF:37, DIRAF:39;
hence
contradiction
by A1, A7, A12, DIRAF:38;
verum
end;
Mid b,o,b2
by A8, DIRAF:def 3;
then
LIN b,o,b2
by DIRAF:34;
then A14:
LIN b2,o,b
by DIRAF:36;
A15:
not LIN o,a2,b2
proof
A16:
LIN b2,
o,
o
by DIRAF:37;
A17:
LIN o,
a2,
o
by DIRAF:37;
assume
LIN o,
a2,
b2
;
contradiction
then
LIN b2,
o,
a
by A7, A12, A17, DIRAF:38;
hence
contradiction
by A1, A14, A13, A16, DIRAF:38;
verum
end;
a2,b2 // b,a
by A9, DIRAF:5;
then A18:
a2,b2 '||' a,b
by DIRAF:def 4;
b <> a
by A1, DIRAF:37;
then A19:
a2,b2 '||' a9,b9
by A4, A18, DIRAF:28;
A20:
a,b // b2,a2
by A9, DIRAF:5;
Mid b,o,b2
by A8, DIRAF:def 3;
then
LIN b,o,b2
by DIRAF:34;
then A21:
LIN o,b,b2
by DIRAF:36;
A22:
LIN o,b,o
by DIRAF:37;
o <> b
by A1, DIRAF:37;
then A23:
LIN o,b2,b9
by A3, A21, A22, DIRAF:38;
then
a2,b2 // b9,a9
by A15, A11, A19, Th12;
then A24:
b2,a2 // a9,b9
by DIRAF:5;
b2,o // o,b9
by A15, A11, A19, A23, Th12;
hence
o,b // o,b9
by A13, A10, DIRAF:6; a,b // a9,b9
a2 <> b2
by A15, DIRAF:37;
hence
a,b // a9,b9
by A20, A24, DIRAF:6; verum