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