theorem Th11: :: FLANG_1:11

for E being set
for a being Element of E ^omega st a ^ a = a holds
a = {}