theorem :: ZF_LANG1:53

for G, H being ZF-formula st G in Subformulae H holds
Subformulae G c= Subformulae H by ZF_LANG:78, ZF_LANG:79;