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 ;
now :: thesis: for x, y being object st x in field (R |_2 Z) & y in field (R |_2 Z) & [x,y] in R |_2 Z holds
[y,x] in R |_2 Z
let x, y be object ; :: 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;
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) ;
hence R |_2 Z is symmetric ; :: thesis: verum