let Y be set ; :: thesis: for R being Relation st R is connected holds
R |_2 Y is connected
let R be Relation; :: thesis: ( R is connected implies R |_2 Y is connected )
assume A1: R is connected ; :: thesis: R |_2 Y is connected

now :: thesis: for a, b being object st a in field (R |_2 Y) & b in field (R |_2 Y) & a <> b & not [a,b] in R |_2 Y holds
[b,a] in R |_2 Y

let a, b be object ; :: thesis: ( a in field (R |_2 Y) & b in field (R |_2 Y) & a <> b & not [a,b] in R |_2 Y implies [b,a] in R |_2 Y )
assume that
A2: ( a in field (R |_2 Y) & b in field (R |_2 Y) ) and
A3: a <> b ; :: thesis: ( [a,b] in R |_2 Y or [b,a] in R |_2 Y )
( a in Y & b in Y ) by A2, Th12;
then A4: ( [a,b] in [:Y,Y:] & [b,a] in [:Y,Y:] ) by ZFMISC_1:87;
( a in field R & b in field R ) by A2, Th12;
then ( [a,b] in R or [b,a] in R ) by A1, A3, Lm4;
hence ( [a,b] in R |_2 Y or [b,a] in R |_2 Y ) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence R |_2 Y is connected by Lm4; :: thesis: verum