theorem :: AFF_4:52

for AS being AffinSpace st AS is not AffinPlane holds
AS is translational