let A be Universal_Algebra; :: thesis: for B being Subset of A
for n, m being Nat st n <= m holds
B |^ n c= B |^ m
let B be Subset of A; :: thesis: for n, m being Nat st n <= m holds
B |^ n c= B |^ m
let n, m be Nat; :: thesis: ( n <= m implies B |^ n c= B |^ m )
assume n <= m ; :: thesis: B |^ n c= B |^ m
then A1: ex i being Nat st m = n + i by NAT_1:10;
defpred S₁[ Nat] means B |^ n c= B |^ (n + $1);
A2: S₁[ 0 ] ;

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

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
deffunc H₁( set , set ) -> set = $2 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= $2 ) } ;
B |^ ((n + i) + 1) = H₁(n,B |^ (n + i)) by Th19;
then B |^ (n + i) c= B |^ (n + (i + 1)) by XBOOLE_1:7;
hence S₁[i + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence B |^ n c= B |^ m by A1; :: thesis: verum