let R be Relation; :: thesis: ( R is strongly_connected iff [:(),():] = R \/ (R ~) )
hereby :: thesis: ( [:(),():] = R \/ (R ~) implies R is strongly_connected )
assume A1: R is strongly_connected ; :: thesis: [:(),():] = R \/ (R ~)
now :: thesis: for x being object holds
( x in [:(),():] iff x in R \/ (R ~) )
let x be object ; :: thesis: ( x in [:(),():] iff x in R \/ (R ~) )
A2: now :: thesis: ( x in R \/ (R ~) implies x in [:(),():] )
assume A3: x in R \/ (R ~) ; :: thesis: x in [:(),():]
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 ;
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 [:(),():] by ; :: thesis: verum
end;
now :: thesis: ( x in [:(),():] implies x in R \/ (R ~) )
assume x in [:(),():] ; :: 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 ; :: thesis: verum
end;
hence ( x in [:(),():] iff x in R \/ (R ~) ) by A2; :: thesis: verum
end;
hence [:(),():] = R \/ (R ~) ; :: thesis: verum
end;
assume A7: [:(),():] = R \/ (R ~) ; :: thesis:
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 ;
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