formula_list(usable).

% inclusion and its relationship to membership

all x y ( i(x,y) <-> ( all v ( e(v,x) -> e(v,y ) ) ) ).

% set difference and its relationship to membership

all v x y ( e(v,d(x,y)) <-> ( e(v,x) & -( e(v,y) ) ) ).

% relationship between set difference and intersection

all x y ( n(x,y) = d(x,d(x,y)) ).

% relationship between null set and set difference

i(0,d(0,0)).

end_of_list.