let V be RealUnitarySpace; :: 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
now :: thesis: for v being VECTOR of V st v in Lin A holds
v 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 Th1;
reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21;
Sum l = v by A2;
hence v in Lin B by Th1; :: thesis: verum
end;
hence Lin A is Subspace of Lin B by RUSUB_1:23; :: thesis: verum