theorem Th39: :: ZF_LANG1:39

for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G by ZF_LANG:def 41, ZF_LANG:62;