for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula st w |= v holds
w is-accepted-by BAutomaton v