for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_left_disjunct_of (F 'or' G) = F & the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )