for X being set
for S being with_empty_element Subset-Family of X
for x being object st x in semidiff S holds
ex A, B being Element of S st x = A \ B