let L be RelStr ; :: thesis: ( L is reflexive implies L is total )
assume L is reflexive ; :: thesis: L is total
then the InternalRel of L is_reflexive_in the carrier of L ;
then dom the InternalRel of L = the carrier of L by ORDERS_1:13;
hence the InternalRel of L is total by PARTFUN1:def 2; :: according to ORDERS_2:def 1 :: thesis: verum