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

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