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