let H be ZF-formula; :: thesis: for x, y, z being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
let x, y, z be Variable; :: thesis: for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
let M be non empty set ; :: thesis: ( M |= H implies M |= Ex (x,y,z,H) )
( M |= H implies M |= Ex (y,z,H) ) by Th96;
hence ( M |= H implies M |= Ex (x,y,z,H) ) by Th94; :: thesis: verum