theorem :: DOMAIN_1:29

for X1 being non empty set
for A1, B1 being Subset of X1 holds A1 \/ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) }