:: deftheorem defines AtomicBasicAsgn MODELC_2:def 61 :
AtomicBasicAsgn = { x where x is Element of ModelSP (Inf_seq AtomicFamily) : ex a being set st x = AtomicAsgn a } ;