let X1 be non empty set ; for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) }
let A1, B1 be Subset of X1; A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) }
A1:
for x1 being Element of X1 holds
( ( not x1 in A1 iff x1 in B1 ) iff ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) )
;
defpred S1[ set ] means ( ( $1 in A1 & not $1 in B1 ) or ( $1 in B1 & not $1 in A1 ) );
defpred S2[ set ] means ( not $1 in A1 iff $1 in B1 );
A2:
A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) }
by Th32;
for X1 being non empty set st ( for x1 being Element of X1 holds
( S2[x1] iff S1[x1] ) ) holds
{ y1 where y1 is Element of X1 : S2[y1] } = { z1 where z1 is Element of X1 : S1[z1] }
from DOMAIN_1:sch 6();
hence
A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) }
by A1, A2; verum