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

A1: now

assume R is strongly_connected ; :: thesis: [:(field R),(field R):] = R \/ (R ~)
then A2: R is_strongly_connected_in field R by Def15;

now

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

A3: now

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

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

now

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

now

let a, 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

end;

then R is_strongly_connected_in field R by Def7;
hence R is strongly_connected by Def15; :: thesis: verum

end;

hence ( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) ) by A1; :: thesis: verum