let A be RelStr ; :: thesis: ( A is strongly_connected implies ( A is reflexive & A is connected ) )
assume A1: A is strongly_connected ; :: thesis: ( A is reflexive & A is connected )
for x being object st x in the carrier of A holds
[x,x] in the InternalRel of A by A1, RELAT_2:def 7;
hence A is reflexive by RELAT_2:def 1, ORDERS_2:def 2; :: thesis: A is connected
for x, y being object st x in the carrier of A & y in the carrier of A & x <> y & not [x,y] in the InternalRel of A holds
[y,x] in the InternalRel of A by A1, RELAT_2:def 7;
hence A is connected by RELAT_2:def 6; :: thesis: verum