let E, x be set ; :: thesis: for A being Subset of ()
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let A be Subset of (); :: thesis: for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )

let k be Nat; :: thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k )
proof
assume <%x%> in A |^.. k ; :: thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) )
then ex m being Nat st
( k <= m & <%x%> in A |^ m ) by Th2;
hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; :: thesis: verum
end;
assume that
A1: <%x%> in A and
A2: ( <%> E in A or k <= 1 ) ; :: thesis: <%x%> in A |^.. k
per cases ( ( <%> E in A & k > 1 ) or k = 0 or k = 1 ) by ;
suppose ( <%> E in A & k > 1 ) ; :: thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by ;
hence <%x%> in A |^.. k by Th2; :: thesis: verum
end;
suppose k = 0 ; :: thesis: <%x%> in A |^.. k
then A |^.. k = A * by Th11;
hence <%x%> in A |^.. k by ; :: thesis: verum
end;
suppose k = 1 ; :: thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by ;
hence <%x%> in A |^.. k by Th2; :: thesis: verum
end;
end;