let a, b be ordinal number ; :: thesis: ( a <> b implies ord-type {a,b} = 2 )
assume a <> b ; :: thesis: ord-type {a,b} = 2
then A1: card {a,b} = 2 by CARD_2:76;
( a c= a \/ b & b c= a \/ b ) by XBOOLE_1:7;
then ( a in succ (a \/ b) & b in succ (a \/ b) ) by ORDINAL1:34;
then A2: {a,b} c= succ (a \/ b) by ZFMISC_1:38;
then On {a,b} = {a,b} by ORDINAL3:8;
hence ord-type {a,b} = 2 by A1, A2, CARD_5:48; :: thesis: verum