theorem Th27: :: AFF_1:28

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS st a,b // A holds
ex c, d being Element of AS st
( c <> d & c in A & d in A & a,b // c,d )