let M be non empty set ; :: thesis: for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds
M |= F1
let F1, F2 be Subset of WFF; :: thesis: ( F1 c= F2 & M |= F2 implies M |= F1 )
assume A1: ( F1 c= F2 & M |= F2 ) ; :: thesis: M |= F1
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in F1 implies M |= H )
assume H in F1 ; :: thesis: M |= H
hence M |= H by A1, Def1; :: thesis: verum