:: deftheorem Def30 defines with_basic MODELC_2:def 30 :
for C being LTLModelStr holds
( C is with_basic iff not the BasicAssign of C is empty );