set MS = the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl;
( the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Euclidean & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Pappian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Desarguesian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Homogeneous & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is translation & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Fanoian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl 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