given i, j being object such that A1: [i,j] in omega ; :: thesis: contradiction
reconsider a = [i,j] as Element of omega by A1;
{} in a by ORDINAL3:8;
hence contradiction by TARSKI:def 2; :: thesis: verum