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 A2: R is strongly_connected ; :: thesis: [:(field R),(field R):] = R \/ (R ~)

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

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

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

assume A4: x in R \/ (R ~) ; :: thesis: x in [:(field R),(field R):]
then consider y, z being set such that
A5: x = [y,z] by RELAT_1:def 1;
( [y,z] in R or [y,z] in R ~ ) by A4, A5, 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 A5, 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 set such that
A6: ( y in field R & z in field R ) and
A7: x = [y,z] by ZFMISC_1:def 2;
( [y,z] in R or [z,y] in R ) by A2, A6, Def7, Def15;
then ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def 7;
hence x in R \/ (R ~) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

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

end;

assume A8: [:(field R),(field R):] = R \/ (R ~) ; :: thesis: R is strongly_connected
let a be set ; :: according to RELAT_2:def 7,RELAT_2:def 15 :: thesis: for y being set st a in field R & y in field R & not [a,y] in R holds
[y,a] in R
let b be set ; :: 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 A8, 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