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

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