set R = SymmetricHull W;
for x being Element of W holds [x,x] in SymmetricHull W

proof

let x be Element of W; :: thesis: [x,x] in SymmetricHull W
x <= x ;
then [x,x] in SymmetricHull W by SymHull;
hence [x,x] in SymmetricHull W ; :: thesis: verum

end;

then T1: SymmetricHull W is reflexive by LATTAD_1:1;
for x, y being object st [x,y] in SymmetricHull W holds
[y,x] in SymmetricHull W

proof

let x, y be object ; :: thesis: ( [x,y] in SymmetricHull W implies [y,x] in SymmetricHull W )
assume A1: [x,y] in SymmetricHull W ; :: thesis: [y,x] in SymmetricHull W
then [x,y] in [: the carrier of W, the carrier of W:] ;
then reconsider x1 = x, y1 = y as Element of W by ZFMISC_1:87;
( x1 <= y1 or y1 <= x1 ) by A1, SymHull;
hence [y,x] in SymmetricHull W by SymHull; :: thesis: verum

end;

hence ( SymmetricHull W is reflexive & SymmetricHull W is symmetric ) by T1, PREFER_1:20; :: thesis: verum