let a be Ordinal; :: thesis: ord-type {a} = 1
a in succ a by ORDINAL1:6;
then A1: {a} c= succ a by ZFMISC_1:31;
then order_type_of (RelIncl {a}) = 1 by CARD_5:37;
hence ord-type {a} = 1 by A1, ORDINAL3:6; :: thesis: verum