let X be set ; :: thesis: ( X is ordinal implies not X is pair )
assume A1: X is ordinal ; :: thesis: not X is pair
assume X is pair ; :: thesis: contradiction
then consider x1, x2 being object such that
A2: X = [x1,x2] by XTUPLE_0:def 1;
X = {{x1,x2},{x1}} by A2, TARSKI:def 5;
hence contradiction by A2, A1; :: thesis: verum