let R be Relation; :: thesis: for X being set st R is_connected_in X holds
R |_2 X is connected
let X be set ; :: thesis: ( 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 ; :: according to RELAT_2:def 6 :: thesis: R |_2 X is connected
let x, y be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: ( 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 ; :: thesis: ( [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; :: thesis: verum