now

A1: {} in 1 by CARD_1:87, TARSKI:def 1;
assume 1 in INT * ; :: thesis: contradiction
then ex x, y being set st {} = [x,y] by A1, RELAT_1:def 1;
hence contradiction ; :: thesis: verum

end;

hence INT <> INT * by INT_1:def 2; :: thesis: verum