theorem :: SEMI_AF1:10

for SAS being Semi_Affine_Space
for a, b, p, q being Element of SAS st not a,b // p,q holds
( a <> b & p <> q ) by Def1, Th3;