let R be non empty RelStr ; :: thesis: ( R is connected iff the InternalRel of R is_strongly_connected_in the carrier of R )
set IR = the InternalRel of R;
set CR = the carrier of R;

hereby :: thesis: ( the InternalRel of R is_strongly_connected_in the carrier of R implies R is connected )

assume A1: R is connected ; :: thesis: the InternalRel of R is_strongly_connected_in the carrier of R

now :: thesis: for x, y being object st x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R

let x, y be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & not [x,y] in the InternalRel of R implies [y,x] in the InternalRel of R )
assume that
A2: x in the carrier of R and
A3: y in the carrier of R ; :: thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
reconsider x9 = x, y9 = y as Element of R by A2, A3;
( x9 <= y9 or y9 <= x9 ) by A1, WAYBEL_0:def 29;
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) ; :: thesis: verum

end;

hence the InternalRel of R is_strongly_connected_in the carrier of R ; :: thesis: verum

end;

assume the InternalRel of R is_strongly_connected_in the carrier of R ; :: thesis: R is connected
then for x, y being Element of R holds
( x <= y or y <= x ) ;
hence R is connected by WAYBEL_0:def 29; :: thesis: verum