formula_list(usable).

% unionset operation U

all y x ( e(y,x) -> i(y,U(x)) ).
all z x y ( e(z,U(x)) -> ( exists y ( e(y,x) & e(z,y) ) ) ).

end_of_list.