theorem Th31: :: AFF_1:32

for AS being AffinSpace
for a, b, p, q being Element of AS
for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds
p,q // A