:: deftheorem Def59 defines AtomicFunc MODELC_2:def 59 :
for a, t being object holds
( ( t in Inf_seq AtomicFamily & a in (CastSeq (t,AtomicFamily)) . 0 implies AtomicFunc (a,t) = TRUE ) & ( ( not t in Inf_seq AtomicFamily or not a in (CastSeq (t,AtomicFamily)) . 0 ) implies AtomicFunc (a,t) = FALSE ) );