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 ;
( ex x being object st x in the carrier of R1 & the InternalRel of R1 is_reflexive_in the carrier of R1 ) by ORDERS_2:def 2, XBOOLE_0:def 1;
hence not the InternalRel of R is empty ; :: according to YELLOW_3:def 3 :: thesis: verum