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

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

hence
A is strongly_connected
by RELAT_2:def 7; :: thesis: verum
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 )

end;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 )
;

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 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;