let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( 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 ; :: thesis: not a,b,d are_collinear

now :: thesis: ( c <> d implies not a,b,d are_collinear )

assume that
A3: c <> d and
A4: a,b,d are_collinear ; :: thesis: 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; :: thesis: verum

end;

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