set V0 = the up-3-dimensional RealLinearSpace;
take ProjectiveSpace the up-3-dimensional RealLinearSpace ; :: thesis: ( ProjectiveSpace the up-3-dimensional RealLinearSpace is transitive & ProjectiveSpace the up-3-dimensional RealLinearSpace is reflexive & ProjectiveSpace the up-3-dimensional RealLinearSpace is proper & ProjectiveSpace the up-3-dimensional RealLinearSpace is Vebleian & ProjectiveSpace the up-3-dimensional RealLinearSpace is at_least_3rank )
thus ( ProjectiveSpace the up-3-dimensional RealLinearSpace is transitive & ProjectiveSpace the up-3-dimensional RealLinearSpace is reflexive & ProjectiveSpace the up-3-dimensional RealLinearSpace is proper & ProjectiveSpace the up-3-dimensional RealLinearSpace is Vebleian & ProjectiveSpace the up-3-dimensional RealLinearSpace is at_least_3rank ) ; :: thesis: verum