let K be Ring; :: thesis: for V being LeftMod of K
for A, B being Subset of V st A c= B holds
Lin A c= Lin B
let V be LeftMod of K; :: thesis: for A, B being Subset of V st A c= B holds
Lin A c= Lin B
let A, B be Subset of V; :: thesis: ( A c= B implies Lin A c= Lin B )
assume A c= B ; :: thesis: Lin A c= Lin B
then Lin A is Subspace of Lin B by MOD_3:17;
hence Lin A c= Lin B by Def7; :: thesis: verum