set M = { (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } ;

now

let u be set ; :: thesis: ( u in { (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } implies u in Bags n )
assume u in { (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } ; :: thesis: u in Bags n
then ex p being Polynomial of n,L st
( u = HT p,T & p in P & p <> 0_ n,L ) ;
hence u in Bags n ; :: thesis: verum

end;

hence { (HT p,T) where p is Polynomial of n,L : ( p in P & p <> 0_ n,L ) } is Subset of (Bags n) by TARSKI:def 3; :: thesis: verum