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

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

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

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

end;now :: thesis: for x being object holds

( x in [:(field R),(field R):] iff x in R \/ (R ~) )

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

end;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;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

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

hence
( x in [:(field R),(field R):] iff x in R \/ (R ~) )
by A2; :: thesis: verumassume
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;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

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