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 = {} )

A7: n > 0 and

A8: A = {} ; :: thesis: A |^.. n = {}

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

assume that
A1:
( A <> {} implies A |^.. n <> {} )

A4: A |^.. n = {} and

A5: ( n <= 0 or A <> {} ) ; :: thesis: contradiction

( n <= 0 implies <%> E in A |^.. n )

end;proof

assume that
assume A2:
A <> {}
; :: thesis: A |^.. n <> {}

end;now :: thesis: for m being Nat holds A |^.. n <> {}

hence
A |^.. n <> {}
; :: thesis: verumlet 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;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

A4: A |^.. n = {} and

A5: ( n <= 0 or A <> {} ) ; :: thesis: contradiction

( n <= 0 implies <%> E in A |^.. n )

proof

hence
contradiction
by A4, A5, A1; :: thesis: verum
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;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

A7: n > 0 and

A8: A = {} ; :: thesis: A |^.. n = {}

now :: thesis: for x being object holds not x in A |^.. n

hence
A |^.. n = {}
by XBOOLE_0:def 1; :: thesis: verumlet 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;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