theorem Th4: :: TRANSLAC:4

for AFP being AffinPlane holds
( AFP is translational iff for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 )