let R be RelStr ; :: thesis: ( not R is empty & R is reflexive implies not R is void )
assume ( not R is empty & R is reflexive ) ; :: thesis: not R is void
then reconsider R1 = R as non empty reflexive RelStr ;
consider x being set such that
A1: x in the carrier of R1 by XBOOLE_0:def 1;
the InternalRel of R1 is_reflexive_in the carrier of R1 by ORDERS_2:def 4;
hence not the InternalRel of R is empty by A1, RELAT_2:def 1; :: according to YELLOW_3:def 3 :: thesis: verum