let AP be AffinPlane; :: thesis: ( AP is Moufangian implies AP is translational )
assume AP is Moufangian ; :: thesis: AP is translational
then AP is satisfying_des_1 by Th3, Th13;
hence AP is translational by Th7; :: thesis: verum