let R be Relation; :: thesis: ( R is reflexive & R is connected implies R is strongly_connected )
assume ( R is reflexive & R is connected ) ; :: thesis: R is strongly_connected
then ( R is_connected_in field R & R is_reflexive_in field R ) by RELAT_2:def 9, RELAT_2:def 14;
hence R is strongly_connected by ORDERS_1:7, RELAT_2:def 15; :: thesis: verum