let E be set ; :: thesis: for A being Subset of (E ^omega)
for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
let A be Subset of (E ^omega); :: thesis: for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
let k be Nat; :: thesis: ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
thus ( not A ? c= A |^.. k or k = 0 or <%> E in A ) :: thesis: ( ( k = 0 or <%> E in A ) implies A ? c= A |^.. k )
proof
A1: <%> E in A ? by FLANG_2:78;
assume A ? c= A |^.. k ; :: thesis: ( k = 0 or <%> E in A )
hence ( k = 0 or <%> E in A ) by A1, Th10; :: thesis: verum
end;
assume ( k = 0 or <%> E in A ) ; :: thesis: A ? c= A |^.. k
then A |^.. k = A * by Th11;
hence A ? c= A |^.. k by FLANG_2:86; :: thesis: verum