let SAS be Semi_Affine_Space; for o, a, b, a', b' being Element of st o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear holds
a,b // a',b'
let o, a, b, a', b' be Element of ; ( o <> a & o <> b & o,a,b is_collinear & o,a,a' is_collinear & o,b,b' is_collinear implies a,b // a',b' )
assume that
A1:
o <> a
and
A2:
o <> b
and
A3:
o,a,b is_collinear
and
A4:
o,a,a' is_collinear
and
A5:
o,b,b' is_collinear
; a,b // a',b'
A6:
now A7:
o,
a // o,
b
by A3, Def2;
o,
a // o,
a'
by A4, Def2;
then A8:
o,
b // o,
a'
by A1, A7, Def1;
o,
b // o,
b'
by A5, Def2;
then
o,
a' // o,
b'
by A2, A8, Def1;
then A9:
o,
a' // a',
b'
by Th18;
o,
b // a,
b
by A7, Th18;
then A10:
a,
b // o,
a'
by A2, A8, Def1;
assume
o <> a'
;
a,b // a',b'hence
a,
b // a',
b'
by A10, A9, Th20;
verum end;
now assume A11:
o = a'
;
a,b // a',b'then
a',
a // a',
b
by A3, Def2;
then A12:
a,
b // a',
b
by Th18;
a',
b // a',
b'
by A5, A11, Def2;
hence
a,
b // a',
b'
by A2, A11, A12, Th20;
verum end;
hence
a,b // a',b'
by A6; verum