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