set M = { b where b is Element of Bags n : ex b9 being bag of n st
( 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
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;
hence { b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } is Subset of (Bags n) by TARSKI:def 3; :: thesis: verum