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 // p,r
let p, q be Element of SAS; :: thesis: ( p <> q implies ex r being Element of SAS st not p,q // p,r )
consider a, b, c being Element of SAS such that
A1: not a,b // a,c by Def1;
assume p <> q ; :: thesis: not for r being Element of SAS holds p,q // p,r
then ( not p,q // p,a or not p,q // p,b or not p,q // p,c ) by A1, Th12;
hence not for r being Element of SAS holds p,q // p,r ; :: thesis: verum