let M be non empty set ; :: thesis: M |= {} WFF
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in {} WFF implies M |= H )
thus ( H in {} WFF implies M |= H ) ; :: thesis: verum