let V be free finite-rank Z_Module; :: thesis: ( rank 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 rank V = 2 )
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume rank 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} ;
{u,v,w} c= I by ;
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;
{u,v} c= I by ;
then A11: I = {u,v} by A7;
then A12: {u,v} is linearly-independent by ;
Lin {u,v} = (Omega). V by ;
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: rank V = 2
A16: {u,v} is Basis of V by ;
card {u,v} = 2 by ;
hence rank V = 2 by ; :: thesis: verum