theorem Th25: :: AOFA_000:25

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