let C be composable with_identities CategoryStr ; :: thesis: ( C is O -ordered implies not C is empty )

assume A1: C is O -ordered ; :: thesis: not C is empty

assume A2: C is empty ; :: thesis: contradiction

consider F being Function such that

A3: F is_isomorphism_of RelOb C, RelIncl O by A1, WELLORD1:def 8;

dom F = field (RelOb C) by A3, WELLORD1:def 7

.= (dom (RelOb C)) \/ (rng (RelOb C)) by RELAT_1:def 6

.= {} by A2 ;

then A4: F = {} ;

field (RelIncl O) = rng F by A3, WELLORD1:def 7;

then (dom (RelIncl O)) \/ (rng (RelIncl O)) = {} by A4, RELAT_1:def 6;

hence contradiction ; :: thesis: verum

assume A1: C is O -ordered ; :: thesis: not C is empty

assume A2: C is empty ; :: thesis: contradiction

consider F being Function such that

A3: F is_isomorphism_of RelOb C, RelIncl O by A1, WELLORD1:def 8;

dom F = field (RelOb C) by A3, WELLORD1:def 7

.= (dom (RelOb C)) \/ (rng (RelOb C)) by RELAT_1:def 6

.= {} by A2 ;

then A4: F = {} ;

field (RelIncl O) = rng F by A3, WELLORD1:def 7;

then (dom (RelIncl O)) \/ (rng (RelIncl O)) = {} by A4, RELAT_1:def 6;

hence contradiction ; :: thesis: verum