let OAS be OAffinSpace; for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )
let o, a, b, a9, b9 be Element of OAS; ( not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 implies ( o,b // o,b9 & a,b // a9,b9 ) )
assume that
A1:
not o,a,b are_collinear
and
A2:
o,a // o,a9
and
A3:
o,b,b9 are_collinear
and
A4:
a,b '||' a9,b9
; ( o,b // o,b9 & a,b // a9,b9 )
A5:
o <> a
by A1, DIRAF:31;
consider a2 being Element of OAS such that
A6:
Mid a,o,a2
and
A7:
o <> a2
by DIRAF:13;
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:2;
a,o // o,a2
by A6, DIRAF:def 3;
then
a2,o // o,a
by DIRAF:2;
then A11:
a2,o // o,a9
by A2, A5, DIRAF:3;
a,o,a2 are_collinear
by A6, DIRAF:28;
then A12:
o,a2,a are_collinear
by DIRAF:30;
A13:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
a2 // a,
b
by A9, DIRAF:2;
then
o,
a2 '||' a,
b
by DIRAF:def 4;
then
(
o,
a2,
o are_collinear &
o,
a2,
b are_collinear )
by A7, A12, DIRAF:31, DIRAF:33;
hence
contradiction
by A1, A7, A12, DIRAF:32;
verum
end;
Mid b,o,b2
by A8, DIRAF:def 3;
then
b,o,b2 are_collinear
by DIRAF:28;
then A14:
b2,o,b are_collinear
by DIRAF:30;
A15:
not o,a2,b2 are_collinear
proof
A16:
b2,
o,
o are_collinear
by DIRAF:31;
A17:
o,
a2,
o are_collinear
by DIRAF:31;
assume
o,
a2,
b2 are_collinear
;
contradiction
then
b2,
o,
a are_collinear
by A7, A12, A17, DIRAF:32;
hence
contradiction
by A1, A14, A13, A16, DIRAF:32;
verum
end;
a2,b2 // b,a
by A9, DIRAF:2;
then A18:
a2,b2 '||' a,b
by DIRAF:def 4;
b <> a
by A1, DIRAF:31;
then A19:
a2,b2 '||' a9,b9
by A4, A18, DIRAF:23;
A20:
a,b // b2,a2
by A9, DIRAF:2;
Mid b,o,b2
by A8, DIRAF:def 3;
then
b,o,b2 are_collinear
by DIRAF:28;
then A21:
o,b,b2 are_collinear
by DIRAF:30;
A22:
o,b,o are_collinear
by DIRAF:31;
o <> b
by A1, DIRAF:31;
then A23:
o,b2,b9 are_collinear
by A3, A21, A22, DIRAF:32;
then
a2,b2 // b9,a9
by A15, A11, A19, Th7;
then A24:
b2,a2 // a9,b9
by DIRAF:2;
b2,o // o,b9
by A15, A11, A19, A23, Th7;
hence
o,b // o,b9
by A13, A10, DIRAF:3; a,b // a9,b9
a2 <> b2
by A15, DIRAF:31;
hence
a,b // a9,b9
by A20, A24, DIRAF:3; verum