set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); :: thesis: ( not L is empty & L is reflexive & L is transitive & L is strongly_connected )
A1: field the Order of {{}} = the carrier of L by ORDERS_1:12;
thus not L is empty ; :: thesis: ( L is reflexive & L is transitive & L is strongly_connected )
thus the InternalRel of L is_reflexive_in the carrier of L by A1, RELAT_2:def 9; :: according to ORDERS_2:def 2 :: thesis: ( L is transitive & L is strongly_connected )
thus the InternalRel of L is_transitive_in the carrier of L by A1, RELAT_2:def 16; :: according to ORDERS_2:def 3 :: thesis: L is strongly_connected
thus the InternalRel of L is_strongly_connected_in the carrier of L by A1, RELAT_2:def 15; :: according to PETERSON:def 2 :: thesis: verum