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