let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, k, l, n being Nat st m <= k & l <= n holds
A |^ k,l c= A |^ m,n
let A be Subset of (E ^omega ); :: thesis: for m, k, l, n being Nat st m <= k & l <= n holds
A |^ k,l c= A |^ m,n
let m, k, l, n be Nat; :: thesis: ( m <= k & l <= n implies A |^ k,l c= A |^ m,n )
assume A1: ( m <= k & l <= n ) ; :: thesis: A |^ k,l c= A |^ m,n
thus A |^ k,l c= A |^ m,n :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ k,l or x in A |^ m,n )
assume x in A |^ k,l ; :: thesis: x in A |^ m,n
then consider kl being Nat such that
A2: ( k <= kl & kl <= l ) and
A3: x in A |^ kl by Th19;
( m <= kl & kl <= n ) by A1, A2, XXREAL_0:2;
hence x in A |^ m,n by A3, Th19; :: thesis: verum

end;