now :: thesis: not 1 in INT *

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

end;

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