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

hereby :: thesis: ( ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies dim V = 2 )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume dim V = 2 ; :: thesis: ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )

then A2: card I = 2 by ;
then consider u being object such that
A3: u in I by ;
reconsider u = u as VECTOR of V by A3;
now :: thesis: not I c= {u}end;
then consider v being object such that
A4: v in I and
A5: not v in {u} ;
reconsider v = v as VECTOR of V by A4;
A6: v <> u by ;
A7: now :: thesis: I c= {u,v}
assume not I c= {u,v} ; :: thesis: contradiction
then consider w being object such that
A8: w in I and
A9: not w in {u,v} ;
for x being object st x in {u,v,w} holds
x in I by ;
then {u,v,w} c= I ;
then A10: card {u,v,w} <= card I by NAT_1:43;
( w <> u & w <> v ) by ;
then 3 <= 2 by ;
hence contradiction ; :: thesis: verum
end;
for x being object st x in {u,v} holds
x in I by ;
then {u,v} c= I ;
then A11: I = {u,v} by A7;
then A12: {u,v} is linearly-independent by ;
Lin {u,v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by
.= (Omega). V by RUSUB_1:def 3 ;
hence ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by ; :: thesis: verum
end;
given u, v being VECTOR of V such that A13: u <> v and
A14: {u,v} is linearly-independent and
A15: (Omega). V = Lin {u,v} ; :: thesis: dim V = 2
Lin {u,v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by ;
then A16: {u,v} is Basis of V by ;
card {u,v} = 2 by ;
hence dim V = 2 by ; :: thesis: verum