let V be non trivial RealLinearSpace; :: thesis: ( ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank ) )
given y, u, v, w being Element of V such that A1: for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ; :: thesis: ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank )
V is up-3-dimensional by A1, Lm42;
hence ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank ) ; :: thesis: verum