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

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