let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds

A is linearly-independent

let A, B be Subset of V; :: thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )

assume that

A1: A c= B and

A2: B is linearly-independent ; :: thesis: A is linearly-independent

let l be Linear_Combination of A; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

reconsider L = l as Linear_Combination of B by A1, RLVECT_2:21;

assume Sum l = 0. V ; :: thesis: Carrier l = {}

then Carrier L = {} by A2;

hence Carrier l = {} ; :: thesis: verum

A is linearly-independent

let A, B be Subset of V; :: thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )

assume that

A1: A c= B and

A2: B is linearly-independent ; :: thesis: A is linearly-independent

let l be Linear_Combination of A; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

reconsider L = l as Linear_Combination of B by A1, RLVECT_2:21;

assume Sum l = 0. V ; :: thesis: Carrier l = {}

then Carrier L = {} by A2;

hence Carrier l = {} ; :: thesis: verum