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