let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st a <> b & a,b,c are_collinear & a,b // c,d holds
c,b // c,d
let a, b, c, d be Element of SAS; :: thesis: ( a <> b & a,b,c are_collinear & a,b // c,d implies c,b // c,d )
assume that
A1: a <> b and
A2: a,b,c are_collinear and
A3: a,b // c,d ; :: thesis: c,b // c,d

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

a,b // a,c by A2;
then A4: ( a,c // c,b & a,c // c,d ) by A1, A3, Def1, Th7;
assume a <> c ; :: thesis: c,b // c,d
hence c,b // c,d by A4, Def1; :: thesis: verum

end;

hence c,b // c,d by A3; :: thesis: verum