let a, b be Ordinal; :: 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:57;
( 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:22;
then A2: {a,b} c= succ (a \/ b) by ZFMISC_1:32;
then On {a,b} = {a,b} by ORDINAL3:6;
hence ord-type {a,b} = 2 by A1, A2, CARD_5:36; :: thesis: verum