:: deftheorem defines disjunctive QC_LANG2:def 10 :
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is disjunctive iff ex p, q being Element of QC-WFF A st H = p 'or' q );