consider CPS being CollProjectiveSpace;
( IncProjSp_of CPS is strict & IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS 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