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

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