let AS be AffinSpace; :: thesis: ( AS is not AffinPlane implies AS is translational )
assume AS is not AffinPlane ; :: thesis: AS is translational
then for A, P, C being Subset of
for a, b, c, a', b', c' being Element of st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c' by Th51;
hence AS is translational by AFF_2:def 11; :: thesis: verum