let O be Ordinal; :: thesis: for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
let X be finite set ; :: thesis: ( X c= O implies order_type_of (RelIncl X) is finite )
assume X c= O ; :: thesis: order_type_of (RelIncl X) is finite
then RelIncl X is well-ordering by WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def 2;
hence order_type_of (RelIncl X) is finite by CARD_3:105; :: thesis: verum