theorem :: REWRITE3:14

for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic