theorem Th36: :: CARD_5:37

for x being object
for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1