let SAS be Semi_Affine_Space; :: thesis: for p, q being Element of SAS st p <> q holds
ex r being Element of SAS st not p,q,r is_collinear
let p, q be Element of SAS; :: thesis: ( p <> q implies ex r being Element of SAS st not p,q,r is_collinear )
assume p <> q ; :: thesis: not for r being Element of SAS holds p,q,r is_collinear
then consider r being Element of SAS such that
A1: not p,q // p,r by Th26;
take r ; :: thesis: not p,q,r is_collinear
thus not p,q,r is_collinear by A1, Def2; :: thesis: verum
thus verum ; :: thesis: verum