let R be Relation; :: thesis: ( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )

hereby :: thesis: ( [:(field R),(field R):] = R \/ (R ~) implies R is strongly_connected )

assume A1: R is strongly_connected ; :: thesis: [:(field R),(field R):] = R \/ (R ~)

now :: thesis: for x being object holds
( x in [:(field R),(field R):] iff x in R \/ (R ~) )

let x be object ; :: thesis: ( x in [:(field R),(field R):] iff x in R \/ (R ~) )

A2: now :: thesis: ( x in R \/ (R ~) implies x in [:(field R),(field R):] )

assume A3: x in R \/ (R ~) ; :: thesis: x in [:(field R),(field R):]
then consider y, z being object such that
A4: x = [y,z] by RELAT_1:def 1;
( [y,z] in R or [y,z] in R ~ ) by A3, A4, XBOOLE_0:def 3;
then ( [y,z] in R or [z,y] in R ) by RELAT_1:def 7;
then ( y in field R & z in field R ) by RELAT_1:15;
hence x in [:(field R),(field R):] by A4, ZFMISC_1:87; :: thesis: verum

end;

now :: thesis: ( x in [:(field R),(field R):] implies x in R \/ (R ~) )

assume x in [:(field R),(field R):] ; :: thesis: x in R \/ (R ~)
then consider y, z being object such that
A5: ( y in field R & z in field R ) and
A6: x = [y,z] by ZFMISC_1:def 2;
( [y,z] in R or [z,y] in R ) by A1, A5, Def7;
then ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def 7;
hence x in R \/ (R ~) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( x in [:(field R),(field R):] iff x in R \/ (R ~) ) by A2; :: thesis: verum

end;

hence [:(field R),(field R):] = R \/ (R ~) ; :: thesis: verum

end;

assume A7: [:(field R),(field R):] = R \/ (R ~) ; :: thesis: R is strongly_connected
let a be object ; :: according to RELAT_2:def 7,RELAT_2:def 15 :: thesis: for y being object st a in field R & y in field R & not [a,y] in R holds
[y,a] in R
let b be object ; :: thesis: ( a in field R & b in field R & not [a,b] in R implies [b,a] in R )
( a in field R & b in field R implies [a,b] in R \/ (R ~) ) by A7, ZFMISC_1:87;
then ( a in field R & b in field R & not [a,b] in R implies [a,b] in R ~ ) by XBOOLE_0:def 3;
hence ( a in field R & b in field R & not [a,b] in R implies [b,a] in R ) by RELAT_1:def 7; :: thesis: verum