let X, Y, Z be set ; :: thesis: for R being Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric
let R be Relation of X,Y; :: thesis: ( R is symmetric implies R |_2 Z is symmetric )
assume R is symmetric ; :: thesis: R |_2 Z is symmetric
then A1: R is_symmetric_in field R by RELAT_2:def 11;

now

let x, y be set ; :: thesis: ( x in field (R |_2 Z) & y in field (R |_2 Z) & [x,y] in R |_2 Z implies [y,x] in R |_2 Z )
assume that
A2: ( x in field (R |_2 Z) & y in field (R |_2 Z) ) and
A3: [x,y] in R |_2 Z ; :: thesis: [y,x] in R |_2 Z
A4: [x,y] in R by A3, XBOOLE_0:def 4;
A5: [y,x] in [:Z,Z:] by A3, ZFMISC_1:88;
( x in field R & y in field R ) by A2, WELLORD1:12;
then [y,x] in R by A1, A4, RELAT_2:def 3;
hence [y,x] in R |_2 Z by A5, XBOOLE_0:def 4; :: thesis: verum

end;

then R |_2 Z is_symmetric_in field (R |_2 Z) by RELAT_2:def 3;
hence R |_2 Z is symmetric by RELAT_2:def 11; :: thesis: verum