:: deftheorem defines |= ZFREFLE1:def 1 :
for M being non empty set
for F being Subset of WFF holds
( M |= F iff for H being ZF-formula st H in F holds
M |= H );