let H be ZF-formula; for x, y, z being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
let x, y, z be Variable; for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
let M be non empty set ; ( M |= H iff M |= All (x,y,z,H) )
( M |= H iff M |= All (y,z,H) )
by Th95;
hence
( M |= H iff M |= All (x,y,z,H) )
by ZF_MODEL:23; verum