theorem Th53: :: AFF_4:53

for AS being AffinSpace
for a, b, c, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )