let A be RelStr ; :: thesis: ( A is reflexive & A is connected implies A is strongly_connected )
assume A1: ( A is reflexive & A is connected ) ; :: thesis: A is strongly_connected
for x, y being object st x in the carrier of A & y in the carrier of A & not [x,y] in the InternalRel of A holds
[y,x] in the InternalRel of A

proof

let x, y be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & not [x,y] in the InternalRel of A implies [y,x] in the InternalRel of A )
assume A2: ( x in the carrier of A & y in the carrier of A ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1, A2, RELAT_2:def 1, ORDERS_2:def 2; :: thesis: verum

end;

suppose x <> y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1, A2, RELAT_2:def 6; :: thesis: verum

end;

end;

end;

hence A is strongly_connected by RELAT_2:def 7; :: thesis: verum