let R be non empty RelStr ; ( 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 ( the InternalRel of R is_strongly_connected_in the carrier of R implies R is connected )
assume A1:
R is
connected
;
the InternalRel of R is_strongly_connected_in the carrier of Rnow 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 Rlet x,
y be
object ;
( 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
;
( [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 )
;
verum end; hence
the
InternalRel of
R is_strongly_connected_in the
carrier of
R
;
verum
end;
assume
the InternalRel of R is_strongly_connected_in the carrier of R
; 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; verum