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