formula_list(usable).

% transitive closure operation T and its relation to powerset 

all x ( e(x,T(x)) ).
all x ( i(T(x),P(T(x))) ).
all x y ( (e(x,y) & i(y,P(y))) -> i(T(x),y) ).

end_of_list.