let V be finite-dimensional RealUnitarySpace; :: thesis: for n being Element of NAT st dim V < n holds
n Subspaces_of V = {}
let n be Element of NAT ; :: thesis: ( dim V < n implies n Subspaces_of V = {} )
assume that
A1: dim V < n and
A2: n Subspaces_of V <> {} ; :: thesis: contradiction
consider x being object such that
A3: x in n Subspaces_of V by A2, XBOOLE_0:def 1;
ex W being strict Subspace of V st
( W = x & dim W = n ) by A3, Def3;
hence contradiction by A1, Th8; :: thesis: verum