Axiomatics of set theory without element relation (Q768277)

The author proposes an axiomatization of set theory based upon the inclusion relation. There are two sorts of variables, one for sets and one for functions. In addition to inclusion, there is only one other primitive predicate, a six-place predicate \(W(a,b,c,d,g,e)\) with the intuitive meaning that the function \(\varphi\) is applicable to the quadruple \((a,b,c,d)\) and yields the value \(e\). On the basis of thirteen axioms, the author begins the development of standard set-theoretic operations and results, reaching the theory of equivalence (one-one correspondences, equinumerous sets, etc.). The given system is shown to be imbeddable in a form of Zermelo-Fraenkel set theory, but the exact relation between the two theories is not made clear (the author claims that the membership relation is not definable in his system). The set theory based upon the given system seems extremely complicated and unwieldy, as compared to the standard systems using the membership relation.