theorem Th52: :: FLANG_2:52

for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ (m,n) = {x} holds
x = <%> E