let C be composable with_identities CategoryStr ; :: thesis: ( C is O -ordered implies C is empty )
assume C is O -ordered ; :: thesis: C is empty
then consider F being Function such that
A1: F is_isomorphism_of RelOb C, RelIncl O by WELLORD1:def 8;
rng F = field (RelIncl O) by A1, WELLORD1:def 7
.= (dom (RelIncl O)) \/ (rng (RelIncl O)) by RELAT_1:def 6
.= {} \/ (rng (RelIncl O))
.= {} ;
then A2: F = {} ;
field (RelOb C) = dom F by A1, WELLORD1:def 7;
then (dom (RelOb C)) \/ (rng (RelOb C)) = {} by A2, RELAT_1:def 6;
hence C is empty ; :: thesis: verum