let a be ordinal number ; :: thesis: ord-type {a} = 1
a in succ a by ORDINAL1:10;
then A1: {a} c= succ a by ZFMISC_1:37;
then order_type_of (RelIncl {a}) = 1 by CARD_5:49;
hence ord-type {a} = 1 by A1, ORDINAL3:8; :: thesis: verum