:: deftheorem defines Consistent HENMODEL:def 3 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds
( f is Consistent iff for p being Element of CQC-WFF Al holds
( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> ) );