theorem :: DOMAIN_1:27

for X1 being non empty set
for A1 being Subset of X1 holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 }