:: deftheorem defines the_right_disjunct_of QC_LANG2:def 15 :
for A being QC-alphabet
for H being Element of QC-WFF A holds the_right_disjunct_of H = the_argument_of (the_right_argument_of (the_argument_of H));