let K be Ring; :: thesis: for V being LeftMod of K
for A being Subset of V holds A c= [#] (Lin A)
let V be LeftMod of K; :: thesis: for A being Subset of V holds A c= [#] (Lin A)
let A be Subset of V; :: thesis: A c= [#] (Lin A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in [#] (Lin A) )
assume x in A ; :: thesis: x in [#] (Lin A)
then x in Lin A by MOD_3:5;
hence x in [#] (Lin A) ; :: thesis: verum