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

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 set ; :: according to TARSKI:def 3 :: thesis: ( x nin B1 |^ (n + 1) or not x nin B2 |^ (n + 1) )
assume A5: ( x in B1 |^ (n + 1) & x nin B2 |^ (n + 1) ) ; :: thesis: contradiction
then reconsider a = x as Element of A ;
a nin B1 |^ n by A5, Th20, A4;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A6: ( a = (Den o,A) . p & p in dom (Den o,A) & rng p c= B1 |^ n ) by A5, Th20;
rng p c= B2 |^ n by A4, A6, XBOOLE_1:1;
hence contradiction by A5, A6, 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