theorem Th8: :: AFF_4:8

for AS being AffinSpace
for a, b, a9, b9, q being Element of AS
for M, N being Subset of AS st q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 holds
q = b9