let A be set ; :: thesis: ( A is ordinal implies not A is pair )
assume A1: ( A is ordinal & A is pair ) ; :: thesis: contradiction
then consider x, y being object such that
A2: A = [x,y] by XTUPLE_0:def 1;
{} in A by A1, ORDINAL3:8;
hence contradiction by A2, TARSKI:def 2; :: thesis: verum