let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st not a,b,c is_collinear & a,b // c,d holds
not a,b,d is_collinear
let a, b, c, d be Element of SAS; :: thesis: ( not a,b,c is_collinear & a,b // c,d implies not a,b,d is_collinear )
assume A1: ( not a,b,c is_collinear & a,b // c,d ) ; :: thesis: not a,b,d is_collinear

now

assume A2: ( c <> d & a,b,d is_collinear ) ; :: thesis: contradiction
A3: ( not a,b // a,c & a,b // c,d & a,c // c,a ) by A1, Def1, Def2;
then A4: ( c <> a & a <> b & a,b // d,c ) by Def1, Th14, Th17;
a,b // a,d by A2, Def2;
then a,b // d,a by Th17;
then ( not c,d // c,a & d,c // d,a ) by A2, A3, A4, Def1, Th29;
hence contradiction by Th18; :: thesis: verum

end;

hence not a,b,d is_collinear by A1; :: thesis: verum