let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
let A be Subset of (E ^omega); :: thesis: for n being Nat st <%> E in A & n > 0 holds
A ? c= A |^ n
let n be Nat; :: thesis: ( <%> E in A & n > 0 implies A ? c= A |^ n )
assume that
A1: <%> E in A and
A2: n > 0 ; :: thesis: A ? c= A |^ n
<%> E in A |^ n by A1, FLANG_1:30;
then A3: {(<%> E)} c= A |^ n by ZFMISC_1:31;
A c= A |^ n by A1, A2, FLANG_1:35;
then {(<%> E)} \/ A c= A |^ n by A3, XBOOLE_1:8;
hence A ? c= A |^ n by Th76; :: thesis: verum