consider MS being Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl;
( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian ) ;
hence ex b₁ being OrtAfSp st
( b₁ is Euclidean & b₁ is Pappian & b₁ is Desarguesian & b₁ is Homogeneous & b₁ is translation & b₁ is Fanoian & b₁ is Moufangian ) ; :: thesis: verum