let E be set ; :: thesis: for A, B, C being Subset of E st ( for x being Element of E holds ( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds A = B \+\ C let A, B, C be Subset of E; :: thesis: ( ( for x being Element of E holds ( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) implies A = B \+\ C ) assume A1:
for x being Element of E holds ( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) )
; :: thesis: A = B \+\ C