:: deftheorem Def29 defines with_basic MODELC_1:def 29 :
for C being CTLModelStr holds
( C is with_basic iff not the BasicAssign of C is empty );