:: deftheorem Def62 defines AtomicKai MODELC_2:def 62 :
for b₁ being Function of atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) holds
( b₁ = AtomicKai iff for a being set st a in atomic_LTL holds
b₁ . a = AtomicAsgn a );