theorem Th83: :: ZF_LANG:83

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