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

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