theorem :: RUSUB_4:14

for V being finite-dimensional RealUnitarySpace holds
( dim V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )