given i, j being set such that A1: [i,j] is Ordinal ; :: thesis: contradiction
{} in {{i},{i,j}} by A1, ORDINAL3:8;
hence contradiction by TARSKI:def 2; :: thesis: verum