let E, x be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat st m > 0 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
let A be Subset of (E ^omega); :: thesis: for m, n being Nat st m > 0 & A |^ (m,n) = {x} holds
for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
let m, n be Nat; :: thesis: ( m > 0 & A |^ (m,n) = {x} implies for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x} )
assume that
A1: m > 0 and
A2: A |^ (m,n) = {x} ; :: thesis: for mn being Nat st m <= mn & mn <= n holds
A |^ mn = {x}
given mn being Nat such that A3: ( m <= mn & mn <= n ) and
A4: A |^ mn <> {x} ; :: thesis: contradiction

per cases ( A |^ mn = {} or A |^ mn <> {} ) ;

suppose A5: A |^ mn = {} ; :: thesis: contradiction

x in A |^ (m,n) by A2, TARSKI:def 1;
then A6: ex i being Nat st
( m <= i & i <= n & x in A |^ i ) by Th19;
A = {} by A5, FLANG_1:27;
hence contradiction by A1, A6, FLANG_1:27; :: thesis: verum

end;

suppose A |^ mn <> {} ; :: thesis: contradiction

then consider y being object such that
A7: y in A |^ mn and
A8: y <> x by A4, ZFMISC_1:35;
y in A |^ (m,n) by A3, A7, Th19;
hence contradiction by A2, A8, TARSKI:def 1; :: thesis: verum

end;

end;