theorem Th30: :: QC_LANG2:30

for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )