for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula holds
( w is-accepted-by BAutomaton v iff w |= v ) by Th68, Th75;