theorem :: ORDINAL6:16

for a, b being Ordinal st a <> b holds
ord-type {a,b} = 2