theorem :: QC_LANG2:38

for A being QC-alphabet
for H being Element of QC-WFF A st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)