theorem Th8: :: SEMI_AF1:8
for SAS being Semi_Affine_Space
for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds
p,q // r,s