let X1 be non empty set ; :: thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) }
let A1, B1 be Subset of X1; :: thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) }
A1: for x1 being Element of X1 holds
( ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) iff ( not x1 in A1 iff x1 in B1 ) ) ;
defpred S₁[ set ] means ( ( $1 in A1 & not $1 in B1 ) or ( not $1 in A1 & $1 in B1 ) );
defpred S₂[ set ] means ( not $1 in A1 iff $1 in B1 );
A2: 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();
A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } by Th61;
hence A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) } by A1, A2; :: thesis: verum