let A be Ordinal; :: thesis: for X being set st X c= A holds
sup X is_cofinal_with order_type_of (RelIncl X)
let X be set ; :: thesis: ( X c= A implies sup X is_cofinal_with order_type_of (RelIncl X) )
assume A1: X c= A ; :: thesis: sup X is_cofinal_with order_type_of (RelIncl X)
then consider phi being Ordinal-Sequence such that
phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) and
A2: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) by Th5;
take phi ; :: according to ORDINAL2:def 17 :: thesis: ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi )
On X = X by A1, ORDINAL3:6;
hence ( dom phi = order_type_of (RelIncl X) & rng phi c= sup X & phi is increasing & sup X = sup phi ) by A2, ORDINAL2:def 3; :: thesis: verum