let H be ZF-formula; 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; for M being non empty set st M |= H holds
M |= Ex (x,y,H)
let M be non empty set ; ( M |= H implies M |= Ex (x,y,H) )
( M |= H implies M |= Ex (y,H) )
by Th94;
hence
( M |= H implies M |= Ex (x,y,H) )
by Th94; verum