defpred S₁[ set ] means ex m being Nat st
( n <= m & $1 = A |^ m );
reconsider M = { B where B is Subset of : S₁[B] } as Subset-Family of from DOMAIN_1:sch 7();
union M is Subset of ;
hence union { B where B is Subset of : ex m being Nat st
( n <= m & B = A |^ m ) } is Subset of ; :: thesis: verum