set M = { b where b is Element of Bags n : ex b9 being bag of n st

( b9 in S & b9 divides b ) } ;

( b9 in S & b9 divides b ) } is Subset of (Bags n) by TARSKI:def 3; :: thesis: verum

( b9 in S & b9 divides b ) } ;

now :: thesis: for u being object st u in { b where b is Element of Bags n : ex b9 being bag of n st

( b9 in S & b9 divides b ) } holds

u in Bags n

hence
{ b where b is Element of Bags n : ex b9 being bag of n st ( b9 in S & b9 divides b ) } holds

u in Bags n

let u be object ; :: thesis: ( u in { b where b is Element of Bags n : ex b9 being bag of n st

( b9 in S & b9 divides b ) } implies u in Bags n )

assume u in { b where b is Element of Bags n : ex b9 being bag of n st

( b9 in S & b9 divides b ) } ; :: thesis: u in Bags n

then ex b being Element of Bags n st

( u = b & ex b9 being bag of n st

( b9 in S & b9 divides b ) ) ;

hence u in Bags n ; :: thesis: verum

end;( b9 in S & b9 divides b ) } implies u in Bags n )

assume u in { b where b is Element of Bags n : ex b9 being bag of n st

( b9 in S & b9 divides b ) } ; :: thesis: u in Bags n

then ex b being Element of Bags n st

( u = b & ex b9 being bag of n st

( b9 in S & b9 divides b ) ) ;

hence u in Bags n ; :: thesis: verum

( b9 in S & b9 divides b ) } is Subset of (Bags n) by TARSKI:def 3; :: thesis: verum