let X1 be non empty set ; :: thesis: 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; :: thesis: 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 S₁[ set ] means ( ( $1 in A1 & not $1 in B1 ) or ( $1 in B1 & not $1 in A1 ) );
defpred S₂[ 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
( S₂[x1] iff S₁[x1] ) ) holds
{ y1 where y1 is Element of X1 : S₂[y1] } = { z1 where z1 is Element of X1 : S₁[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; :: thesis: verum