theorem Th53: :: FLANG_2:53

for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat holds
( <%x%> in A |^ (m,n) iff ( <%x%> in A & m <= n & ( ( <%> E in A & n > 0 ) or ( m <= 1 & 1 <= n ) ) ) )