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