theorem Th12: :: SEMI_AF1:12

for SAS being Semi_Affine_Space
for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds
not p,q // p,c