:: deftheorem defines |= MODELC_2:def 64 :
for r being Element of Inf_seq AtomicFamily
for W being Subset of LTL_WFF holds
( r |= W iff for H being LTL-formula st H in W holds
r |= H );