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} ) )

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 A15, RUSUB_1:def 3;

then A16: {u,v} is Basis of V by A14, RUSUB_3:def 2;

card {u,v} = 2 by A13, CARD_2:57;

hence dim V = 2 by A16, Def2; :: thesis: verum

( 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 )

given u, v being VECTOR of V such that A13:
u <> v
and ( 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;

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;

x in I by A3, A4, TARSKI:def 2;

then {u,v} c= I ;

then A11: I = {u,v} by A7;

then A12: {u,v} is linearly-independent by A1, RUSUB_3:def 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 A1, A11, RUSUB_3:def 2

.= (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 A6, A12; :: thesis: verum

end;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}

then consider v being object such that 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 card I <= card {u} by NAT_1:43;

then 2 <= 1 by A2, CARD_1:30;

hence contradiction ; :: thesis: verum

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}

for x being object st x in {u,v} holds 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;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

x in I by A3, A4, TARSKI:def 2;

then {u,v} c= I ;

then A11: I = {u,v} by A7;

then A12: {u,v} is linearly-independent by A1, RUSUB_3:def 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 A1, A11, RUSUB_3:def 2

.= (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 A6, A12; :: thesis: verum

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 A15, RUSUB_1:def 3;

then A16: {u,v} is Basis of V by A14, RUSUB_3:def 2;

card {u,v} = 2 by A13, CARD_2:57;

hence dim V = 2 by A16, Def2; :: thesis: verum