let E be set ; :: thesis: for A being Subset of (E ^omega)
for n, m being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m
let A be Subset of (E ^omega); :: thesis: for n, m being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m
let n, m be Nat; :: thesis: ( <%> E in A & m > n implies A |^ n c= A |^ m )
assume that
A1: <%> E in A and
A2: m > n ; :: thesis: A |^ n c= A |^ m
consider k being Nat such that
A3: n + k = m by A2, NAT_1:10;
<%> E in A |^ k by A1, Th30;
then A |^ n c= (A |^ k) ^^ (A |^ n) by Th16;
hence A |^ n c= A |^ m by A3, Th33; :: thesis: verum