theorem Th4: :: FLANG_2:4

for E being set
for a, b being Element of E ^omega st ( a ^ b = a or b ^ a = a ) holds
b = {}