let x be object ; :: thesis: for O being Ordinal st {x} c= O holds
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x
let O be Ordinal; :: thesis: ( {x} c= O implies canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x )
set X = {x};
set R = RelIncl {x};
set C = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}));
A1: RelIncl {0} = {[0,0]} by WELLORD2:22;
assume A2: {x} c= O ; :: thesis: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x
then A3: order_type_of (RelIncl {x}) = {0} by Th36, CARD_1:49;
RelIncl {x} is well-ordering by A2, WELLORD2:8;
then RelIncl {x}, RelIncl (order_type_of (RelIncl {x})) are_isomorphic by WELLORD2:def 2;
then A4: RelIncl (order_type_of (RelIncl {x})), RelIncl {x} are_isomorphic by WELLORD1:40;
RelIncl (order_type_of (RelIncl {x})) is well-ordering by WELLORD2:8;
then A5: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) is_isomorphism_of RelIncl (order_type_of (RelIncl {x})), RelIncl {x} by A4, WELLORD1:def 9;
then A6: rng (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {x}) by A3, WELLORD1:def 7
.= {x} by WELLORD2:def 1 ;
dom (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {x}))) = field (RelIncl {0}) by A5, A3, WELLORD1:def 7
.= {0} by A1, RELAT_1:173 ;
hence canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x})) = 0 .--> x by A3, A6, FUNCT_4:112; :: thesis: verum