theorem Th6: :: ZFREFLE1:6

for H being ZF-formula ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )