let P be RelStr ; :: thesis: ( P is empty implies P is total )
assume A1: the carrier of P is empty ; :: according to STRUCT_0:def 1 :: thesis: P is total
hence dom the InternalRel of P = dom {}
.= the carrier of P by A1 ;
:: according to PARTFUN1:def 2,ORDERS_2:def 1 :: thesis: verum