let A be Universal_Algebra; :: thesis: for B1, B2 being Subset of A st B1 c= B2 holds
for n being Nat holds B1 |^ n c= B2 |^ n
let B1, B2 be Subset of A; :: thesis: ( B1 c= B2 implies for n being Nat holds B1 |^ n c= B2 |^ n )
assume A1: B1 c= B2 ; :: thesis: for n being Nat holds B1 |^ n c= B2 |^ n
defpred S₁[ Nat] means B1 |^ $1 c= B2 |^ $1;
B1 |^ 0 = B1 by Th18;
then A2: S₁[ 0 ] by A1, Th18;

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin B1 |^ (n + 1) or not x nin B2 |^ (n + 1) )
assume that
A5: x in B1 |^ (n + 1) and
A6: x nin B2 |^ (n + 1) ; :: thesis: contradiction
reconsider a = x as Element of A by A5;
a nin B1 |^ n by A4, A6, Th20;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A7: a = (Den (o,A)) . p and
A8: p in dom (Den (o,A)) and
A9: rng p c= B1 |^ n by A5, Th20;
rng p c= B2 |^ n by A4, A9, XBOOLE_1:1;
hence contradiction by A6, A7, A8, Th20; :: thesis: verum

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Nat holds B1 |^ n c= B2 |^ n ; :: thesis: verum