let V be RealLinearSpace; :: thesis: for A, B being Subset of V st A c= the carrier of (Lin B) holds
Lin A is Subspace of Lin B
let A, B be Subset of V; :: thesis: ( A c= the carrier of (Lin B) implies Lin A is Subspace of Lin B )
assume A1: A c= the carrier of (Lin B) ; :: thesis: Lin A is Subspace of Lin B
reconsider D = the carrier of (Lin B) as Subset of V by RLSUB_1:def 2;
Lin A is Subspace of Lin D by RLVECT_3:20, A1;
hence Lin A is Subspace of Lin B by RLVECT_3:18; :: thesis: verum