theorem :: MODELC_2:63

for H being LTL-formula
for r being Element of Inf_seq AtomicFamily st H is atomic holds
( r |= H iff H in (CastSeq (r,AtomicFamily)) . 0 )