let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st not a,b,c are_collinear & a,b // c,d holds
not a,b,d are_collinear
let a, b, c, d be Element of SAS; ( not a,b,c are_collinear & a,b // c,d implies not a,b,d are_collinear )
assume that
A1:
not a,b,c are_collinear
and
A2:
a,b // c,d
; not a,b,d are_collinear
now ( c <> d implies not a,b,d are_collinear )assume that A3:
c <> d
and A4:
a,
b,
d are_collinear
;
contradiction
a,
b // a,
d
by A4;
then A5:
a,
b // d,
a
by Th6;
A6:
a,
b // d,
c
by A2, Th6;
A7:
a,
c // c,
a
by Def1;
A8:
not
a,
b // a,
c
by A1;
then
a <> b
by Th3;
then A9:
d,
c // d,
a
by A6, A5, Def1;
c <> a
by A8, Def1;
then
not
c,
d // c,
a
by A2, A3, A8, A7, Th15;
hence
contradiction
by A9, Th7;
verum end;
hence
not a,b,d are_collinear
by A1; verum