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

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