let R be Ring; :: thesis: for V being LeftMod of R

for A being Subset of V holds A is Subset of (Lin A)

let V be LeftMod of R; :: thesis: for A being Subset of V holds A is Subset of (Lin A)

let A be Subset of V; :: thesis: A is Subset of (Lin A)

for x being object st x in A holds

x in the carrier of (Lin A)

hence A is Subset of (Lin A) ; :: thesis: verum

for A being Subset of V holds A is Subset of (Lin A)

let V be LeftMod of R; :: thesis: for A being Subset of V holds A is Subset of (Lin A)

let A be Subset of V; :: thesis: A is Subset of (Lin A)

for x being object st x in A holds

x in the carrier of (Lin A)

proof

then
A c= the carrier of (Lin A)
;
let x be object ; :: thesis: ( x in A implies x in the carrier of (Lin A) )

assume A1: x in A ; :: thesis: x in the carrier of (Lin A)

x in Lin A by A1, MOD_3:5;

hence x in the carrier of (Lin A) ; :: thesis: verum

end;assume A1: x in A ; :: thesis: x in the carrier of (Lin A)

x in Lin A by A1, MOD_3:5;

hence x in the carrier of (Lin A) ; :: thesis: verum

hence A is Subset of (Lin A) ; :: thesis: verum