let K be Ring; :: thesis: for V being LeftMod of
for A, B being Subset of st A c= B holds
Lin A c= Lin B
let V be LeftMod of ; :: thesis: for A, B being Subset of st A c= B holds
Lin A c= Lin B
let A, B be Subset of ; :: 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