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

end;

now

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

end;

now

assume A7: [:(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 A7, ZFMISC_1:106;
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