set CPS = the CollProjectiveSpace;
( IncProjSp_of the CollProjectiveSpace is strict & IncProjSp_of the CollProjectiveSpace is partial & IncProjSp_of the CollProjectiveSpace is linear & IncProjSp_of the CollProjectiveSpace is up-2-dimensional & IncProjSp_of the CollProjectiveSpace is up-3-rank & IncProjSp_of the CollProjectiveSpace is Vebleian ) ;
hence ex b₁ being IncProjStr st
( b₁ is strict & b₁ is partial & b₁ is linear & b₁ is up-2-dimensional & b₁ is up-3-rank & b₁ is Vebleian ) ; :: thesis: verum