theorem Th16: :: SEMI_AF1:16

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