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

let x, y be set ; :: 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 x' = x, y' = y as Element of R by A2, A3;
( x' <= y' or y' <= x' ) by A1, WAYBEL_0:def 29;
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by ORDERS_2:def 9; :: thesis: verum

end;

hence the InternalRel of R is_strongly_connected_in the carrier of R by RELAT_2:def 7; :: thesis: verum

end;

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

now

let x, y be Element of R; :: thesis: ( x <= y or y <= x )
( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A4, RELAT_2:def 7;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: thesis: verum

end;

hence R is connected by WAYBEL_0:def 29; :: thesis: verum