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 that
A1: not a,b,c is_collinear and
A2: a,b // c,d ; :: thesis: not a,b,d is_collinear

now

assume that
A3: c <> d and
A4: a,b,d is_collinear ; :: thesis: contradiction
a,b // a,d by A4, Def2;
then A5: a,b // d,a by Th17;
A6: a,b // d,c by A2, Th17;
A7: a,c // c,a by Def1;
A8: not a,b // a,c by A1, Def2;
then a <> b by Th14;
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, Th29;
hence contradiction by A9, Th18; :: thesis: verum

end;

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