let V be finite-dimensional RealLinearSpace; :: 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 A1, Def2;
then consider u being object such that
A3: u in I by CARD_1:27, XBOOLE_0:def 1;
reconsider u = u as VECTOR of V by A3;

now :: thesis: not I c= {u}

assume I c= {u} ; :: thesis: contradiction
then card I <= card {u} by NAT_1:43;
then 2 <= 1 by A2, CARD_1:30;
hence contradiction ; :: thesis: verum

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 A5, TARSKI:def 1;

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 A3, A4, A8, ENUMSET1:def 1;
then {u,v,w} c= I ;
then A10: card {u,v,w} <= card I by NAT_1:43;
( w <> u & w <> v ) by A9, TARSKI:def 2;
then 3 <= 2 by A2, A6, A10, CARD_2:58;
hence contradiction ; :: thesis: verum

end;

for x being object st x in {u,v} holds
x in I by A3, A4, TARSKI:def 2;
then {u,v} c= I ;
then A11: I = {u,v} by A7, XBOOLE_0:def 10;
then A12: {u,v} is linearly-independent by A1, RLVECT_3:def 3;
Lin {u,v} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by A1, A11, RLVECT_3:def 3
.= (Omega). V by RLSUB_1:def 4 ;
hence ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; :: 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} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by A15, RLSUB_1:def 4;
then A16: {u,v} is Basis of V by A14, RLVECT_3:def 3;
card {u,v} = 2 by A13, CARD_2:57;
hence dim V = 2 by A16, Def2; :: thesis: verum