theorem Th8: :: FSM_3:8

for E being non empty set holds not <%> E in Lex E