theorem Th55: :: ZF_LANG1:55

for F, G being ZF-formula holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}