:: deftheorem Def63 defines |= MODELC_2:def 63 :
for r being Element of Inf_seq AtomicFamily
for H being LTL-formula holds
( r |= H iff r |= Evaluate (H,AtomicKai) );