let R be RelStr ; :: thesis: ( R is empty implies ( R is reflexive & R is antisymmetric & R is transitive & R is connected & R is strongly_connected ) )
assume A1: R is empty ; :: thesis: ( R is reflexive & R is antisymmetric & R is transitive & R is connected & R is strongly_connected )
then the InternalRel of R = {} ;
then field the InternalRel of R = the carrier of R by A1, RELAT_1:40;
then ( the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is_antisymmetric_in the carrier of R & the InternalRel of R is_transitive_in the carrier of R & the InternalRel of R is_connected_in the carrier of R & the InternalRel of R is_strongly_connected_in the carrier of R ) by A1, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16, RELAT_2:def 14, RELAT_2:def 15;
hence ( R is reflexive & R is antisymmetric & R is transitive & R is connected & R is strongly_connected ) by ORDERS_2:def 2, ORDERS_2:def 4, ORDERS_2:def 3; :: thesis: verum