theorem :: DOMAIN_1:22

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