set M = { b where b is Element of Bags n : ex b' being bag of st
( b' in S & b' divides b ) } ;

now

let u be set ; :: thesis: ( u in { b where b is Element of Bags n : ex b' being bag of st
( b' in S & b' divides b ) } implies u in Bags n )
assume u in { b where b is Element of Bags n : ex b' being bag of st
( b' in S & b' divides b ) } ; :: thesis: u in Bags n
then consider b being Element of Bags n such that
A1: ( u = b & ex b' being bag of st
( b' in S & b' divides b ) ) ;
thus u in Bags n by A1; :: thesis: verum

end;

hence { b where b is Element of Bags n : ex b' being bag of st
( b' in S & b' divides b ) } is Subset of (Bags n) by TARSKI:def 3; :: thesis: verum