let MS be OrtAfPl; :: thesis: ( MS is Euclidean & MS is Desarguesian implies MS is Pappian )
assume ( MS is Euclidean & MS is Desarguesian ) ; :: thesis: MS is Pappian
then ( MS is satisfying_3H & MS is satisfying_DES ) by Th8, Th11;
then MS is satisfying_PAP by CONMETR:13, CONMETR:15;
hence MS is Pappian by Th10; :: thesis: verum