let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {} iff ( n > 0 & A = {} ) )
let A be Subset of (E ^omega); :: thesis: for n being Nat holds
( A |^.. n = {} iff ( n > 0 & A = {} ) )
let n be Nat; :: thesis: ( A |^.. n = {} iff ( n > 0 & A = {} ) )
thus ( A |^.. n = {} implies ( n > 0 & A = {} ) ) :: thesis: ( n > 0 & A = {} implies A |^.. n = {} )
proof
A1: ( A <> {} implies A |^.. n <> {} )
proof
assume A2: A <> {} ; :: thesis: A |^.. n <> {}
now :: thesis: for m being Nat holds A |^.. n <> {}
let m be Nat; :: thesis: A |^.. n <> {}
consider m being Nat such that
A3: n <= m ;
A |^ m <> {} by A2, FLANG_1:27;
then ex x being object st x in A |^ m by XBOOLE_0:def 1;
hence A |^.. n <> {} by A3, Th2; :: thesis: verum
end;
hence A |^.. n <> {} ; :: thesis: verum
end;
assume that
A4: A |^.. n = {} and
A5: ( n <= 0 or A <> {} ) ; :: thesis: contradiction
( n <= 0 implies <%> E in A |^.. n )
proof
assume n <= 0 ; :: thesis: <%> E in A |^.. n
then A6: n = 0 ;
A |^ 0 c= A |^.. 0 by Th3;
then {(<%> E)} c= A |^.. 0 by FLANG_1:24;
hence <%> E in A |^.. n by A6, ZFMISC_1:31; :: thesis: verum
end;
hence contradiction by A4, A5, A1; :: thesis: verum
end;
assume that
A7: n > 0 and
A8: A = {} ; :: thesis: A |^.. n = {}
now :: thesis: for x being object holds not x in A |^.. n
let x be object ; :: thesis: not x in A |^.. n
assume x in A |^.. n ; :: thesis: contradiction
then ex m being Nat st
( n <= m & x in A |^ m ) by Th2;
hence contradiction by A7, A8, FLANG_1:27; :: thesis: verum
end;
hence A |^.. n = {} by XBOOLE_0:def 1; :: thesis: verum