let V be Z_Module; :: 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

let x be object ; :: thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; :: thesis: x in the carrier of (Lin A)
then x in Lin A by ZMODUL02:65;
hence x in the carrier of (Lin A) ; :: thesis: verum

end;

then A c= the carrier of (Lin A) ;
hence A is Subset of (Lin A) ; :: thesis: verum