theorem Th91: :: QC_LANG2:91

for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}