set a = y;
set b = x;
set f = (x,y) --> (y,x);
reconsider R = (x,y) --> (y,x) as Relation ;
per cases ( x = y or x <> y ) ;
suppose x = y ; :: thesis: [:{x},{y}:] +* [:{y},{x}:] is symmetric
then A1: (x,y) --> (y,x) = {[x,x]} by ZFMISC_1:29;
{[x,x]} \+\ (id {x}) = {} ;
hence [:{x},{y}:] +* [:{y},{x}:] is symmetric by A1, Th29; :: thesis: verum
end;
suppose A2: x <> y ; :: thesis: [:{x},{y}:] +* [:{y},{x}:] is symmetric
A3: (x,y) --> (y,x) = [:{x},{y}:] +* [:{y},{x}:]
.= ([:{x},{y}:] | {x}) \/ [:{y},{x}:] by ZFMISC_1:14, A2
.= [:{x},{y}:] \/ [:{y},{x}:] ;
R ~ = ([:{x},{y}:] ~) \/ ([:{y},{x}:] ~) by RELAT_1:23, A3
.= ([:{x},{y}:] ~) \/ [:{x},{y}:] by SYSREL:5
.= R by A3, SYSREL:5 ;
hence [:{x},{y}:] +* [:{y},{x}:] is symmetric by RELAT_2:13; :: thesis: verum
end;
end;