let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, l, m, 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 k, l, m, n being Nat st m <= k & l <= n holds
A |^ (k,l) c= A |^ (m,n)
let k, l, m, 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 object ; :: 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;