let R be Relation; ( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) )
hereby ( [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) implies R is connected )
assume
R is
connected
;
[:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)then A1:
R is_connected_in field R
;
now for x being object st x in [:(field R),(field R):] \ (id (field R)) holds
x in R \/ (R ~)let x be
object ;
( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~) )now ( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~) )assume A2:
x in [:(field R),(field R):] \ (id (field R))
;
x in R \/ (R ~)then
x in [:(field R),(field R):]
by XBOOLE_0:def 5;
then consider y,
z being
object such that A3:
y in field R
and A4:
z in field R
and A5:
x = [y,z]
by ZFMISC_1:def 2;
not
x in id (field R)
by A2, XBOOLE_0:def 5;
then
y <> z
by A3, A5, RELAT_1:def 10;
then
(
[y,z] in R or
[z,y] in R )
by A1, A3, A4;
then
(
[y,z] in R or
[y,z] in R ~ )
by RELAT_1:def 7;
hence
x in R \/ (R ~)
by A5, XBOOLE_0:def 3;
verum end; hence
(
x in [:(field R),(field R):] \ (id (field R)) implies
x in R \/ (R ~) )
;
verum end; hence
[:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)
;
verum
end;
assume A6:
[:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)
; R is connected
let a be object ; RELAT_2:def 6,RELAT_2:def 14 for y being object st a in field R & y in field R & a <> y & not [a,y] in R holds
[y,a] in R
let b be object ; ( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R )
( [a,b] in [:(field R),(field R):] \ (id (field R)) implies [a,b] in R \/ (R ~) )
by A6;
then
( [a,b] in [:(field R),(field R):] & not [a,b] in id (field R) implies [a,b] in R \/ (R ~) )
by XBOOLE_0:def 5;
then
( a in field R & b in field R & a <> b & not [a,b] in R implies [a,b] in R ~ )
by RELAT_1:def 10, XBOOLE_0:def 3, ZFMISC_1:87;
hence
( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R )
by RELAT_1:def 7; verum