for A being QC-alphabet
for H being Element of QC-WFF A st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)