for A being Universal_Algebra
for B being Subset of A ex C being Subset of A st
( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )