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

let a, b be set ; :: 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 ( a in field (R |_2 Y) & b in field (R |_2 Y) & a <> b ) ; :: thesis: ( [a,b] in R |_2 Y or [b,a] in R |_2 Y )
then A2: ( a in field R & b in field R & a in Y & b in Y & a <> b ) by Th19;
then A3: ( [a,b] in R or [b,a] in R ) by A1, Lm4;
( [a,b] in [:Y,Y:] & [b,a] in [:Y,Y:] ) by A2, ZFMISC_1:106;
hence ( [a,b] in R |_2 Y or [b,a] in R |_2 Y ) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

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