let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A c= B holds

Lin A is Subspace of Lin B

let A, B be Subset of V; :: thesis: ( A c= B implies Lin A is Subspace of Lin B )

assume A1: A c= B ; :: thesis: Lin A is Subspace of Lin B

Lin A is Subspace of Lin B

let A, B be Subset of V; :: thesis: ( A c= B implies Lin A is Subspace of Lin B )

assume A1: A c= B ; :: thesis: Lin A is Subspace of Lin B

now :: thesis: for v being VECTOR of V st v in Lin A holds

v in Lin B

hence
Lin A is Subspace of Lin B
by RLSUB_1:29; :: thesis: verumv in Lin B

let v be VECTOR of V; :: thesis: ( v in Lin A implies v in Lin B )

assume v in Lin A ; :: thesis: v in Lin B

then consider l being Linear_Combination of A such that

A2: v = Sum l by Th14;

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

Sum l = v by A2;

hence v in Lin B by Th14; :: thesis: verum

end;assume v in Lin A ; :: thesis: v in Lin B

then consider l being Linear_Combination of A such that

A2: v = Sum l by Th14;

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

Sum l = v by A2;

hence v in Lin B by Th14; :: thesis: verum