for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for A being non empty automaton over F holds
( w in Lang A iff ex p, q being Element of A st
( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )