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 Lm5;
then reconsider o = order_type_of (RelIncl X) as natural number ;
card X = card (order_type_of (RelIncl X)) by A1, Th16;
then o = card X by CARD_1:def 2;
hence order_type_of (RelIncl X) = card X ; :: thesis: verum