for A being Universal_Algebra
for B1, B2 being Subset of A st B1 c= B2 holds
for n being Nat holds B1 |^ n c= B2 |^ n