let V be non trivial RealLinearSpace; ( 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 )
; ( 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 )
; verum