let O be Ordinal; :: thesis: for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X
let X be finite set ; :: thesis: ( X c= O implies order_type_of (RelIncl X) = card X )
assume A1: X c= O ; :: thesis: order_type_of (RelIncl X) = card X
then order_type_of (RelIncl X) is finite by Lm4;
then reconsider o = order_type_of (RelIncl X) as Nat ;
card X = card (order_type_of (RelIncl X)) by A1, Th7;
then o = card X ;
hence order_type_of (RelIncl X) = card X ; :: thesis: verum