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

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

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

then A3: A = {} by FLANG_1:28;
x in A |^ m,n by A1, TARSKI:def 1;
then consider i being Nat such that
A4: ( m <= i & i <= n & x in A |^ i ) by Th19;
thus contradiction by A1, A3, A4, FLANG_1:28; :: thesis: verum

end;

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

then consider y being set such that
A5: ( y in A |^ mn & y <> x ) by A2, ZFMISC_1:41;
y in A |^ m,n by A2, A5, Th19;
hence contradiction by A1, A5, TARSKI:def 1; :: thesis: verum

end;

end;