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