X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then INT \ {0} <> {} by X1, XBOOLE_0:def 5;
hence not [: the carrier of V,(INT \ {0}):] is empty ; :: thesis: verum