let x be object ; :: thesis: for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1
let O be Ordinal; :: thesis: ( {x} c= O implies order_type_of (RelIncl {x}) = 1 )
card {x} = 1 by CARD_2:42;
hence ( {x} c= O implies order_type_of (RelIncl {x}) = 1 ) by Th35; :: thesis: verum