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

now :: thesis: for u being object st u in { (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } holds
u in Bags n

let u be object ; :: 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