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 A2: card X = card (order_type_of (RelIncl X)) by CARD_5:16;
order_type_of (RelIncl X) is finite by A1, Lm1;
then order_type_of (RelIncl X) in omega by CARD_1:103;
then reconsider o = order_type_of (RelIncl X) as natural number ;
o = card X by A2, CARD_1:def 5;
hence order_type_of (RelIncl X) = card X ; :: thesis: verum