theorem Th15: :: SEMI_AF1:15
for SAS being Semi_Affine_Space
for a, b, c, d, p, q, r, s being Element of SAS st not a,b // c,d & a,b // p,q & c,d // r,s & p <> q & r <> s holds
not p,q // r,s