let R be Relation; for X being set st R is_connected_in X holds
R |_2 X is connected
let X be set ; ( R is_connected_in X implies R |_2 X is connected )
assume A1:
for x, y being object st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R
; RELAT_2:def 6 R |_2 X is connected
let x, y be object ; RELAT_2:def 6,RELAT_2:def 14 ( not x in field (R |_2 X) or not y in field (R |_2 X) or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A2:
x in field (R |_2 X)
and
A3:
y in field (R |_2 X)
and
A4:
x <> y
; ( [x,y] in R |_2 X or [y,x] in R |_2 X )
A5:
y in X
by A3, WELLORD1:12;
A6:
x in X
by A2, WELLORD1:12;
then A7:
[x,y] in [:X,X:]
by A5, ZFMISC_1:87;
A8:
[y,x] in [:X,X:]
by A6, A5, ZFMISC_1:87;
( [x,y] in R or [y,x] in R )
by A1, A4, A6, A5;
hence
( [x,y] in R |_2 X or [y,x] in R |_2 X )
by A7, A8, XBOOLE_0:def 4; verum