for E being non empty set
for TS being transition-system over Lex E st the Tran of TS is Function holds
TS is deterministic