let x be set ; :: 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});
assume A1: {x} c= O ; :: thesis: canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}) = 0 .--> x
then RelIncl {x} is well-ordering by WELLORD2:9;
then RelIncl {x}, RelIncl (order_type_of (RelIncl {x})) are_isomorphic by WELLORD2:def 2;
then A2: RelIncl (order_type_of (RelIncl {x})), RelIncl {x} are_isomorphic by WELLORD1:50;
RelIncl (order_type_of (RelIncl {x})) is well-ordering by WELLORD2:9;
then A3: canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}) is_isomorphism_of RelIncl (order_type_of (RelIncl {x})), RelIncl {x} by A2, WELLORD1:def 9;
A4: RelIncl {0 } = {[0 ,0 ]} by Th5;
A5: order_type_of (RelIncl {x}) = {0 } by A1, Th14, CARD_1:87;
then A6: dom (canonical_isomorphism_of (RelIncl {0 }),(RelIncl {x})) = field (RelIncl {0 }) by A3, WELLORD1:def 7
.= {0 } by A4, Th2 ;
rng (canonical_isomorphism_of (RelIncl {0 }),(RelIncl {x})) = field (RelIncl {x}) by A3, A5, WELLORD1:def 7
.= {x} by WELLORD2:def 1 ;
hence canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}) = 0 .--> x by A5, A6, Th1; :: thesis: verum