theorem Th21: :: AOFA_000:21

for A being Universal_Algebra
for B being Subset of A
for n, m being Nat st n <= m holds
B |^ n c= B |^ m