The subset relation and $2$-stratified sentences in set theory and class theory

Hamkins and Kikuchi (2016 and 2017) show that in both set theory and class theory the definable subset ordering of the universe interprets a complete and decidable theory. If $\mathcal{M}$ is a model of set theory, then $\langle M, \subseteq^$\mathcal{M}$ \rangle$ is an atomic unbounded relatively complemented distributive lattice. If $\mathcal{M}$ is model of class theory, then $\langle M, \subseteq^$\mathcal{M}$ \rangle$ is an infinite atomic boolean algebra. We identify the minimal subsystem of $\mathrm{Z}\mathrm{F}$, $\mathrm{B}\mathrm{A}\mathrm{S}$, that ensures that the definable subset relation is an atomic unbounded relatively complemented distributive lattice and classify the atomic unbounded relatively complemented distributive lattices that can be realised as a subset relations of this theory. The fact that the theory of atomic unbounded relatively complemented distributive lattices is complete is used to show that $\mathrm{B}\mathrm{A}\mathrm{S}$ decides every $2$-stratified sentence of set theory. We also identify the minimal subsystem of $\mathrm{N}\mathrm{B}\mathrm{G}$, $\mathrm{B}\mathrm{A}\mathrm{C}$, that ensures that the definable subset relation is an infinite atomic Boolean algebra. We show that there is a complete extension, ${\mathrm{I}\mathrm{A}\mathrm{B}\mathrm{A}}_{\mathrm{I}\mathrm{d}\mathrm{e}\mathrm{a}\mathrm{l}}$, of the theory of infinite atomic boolean algebras and an extension ${\mathrm{B}\mathrm{A}\mathrm{C}}^{+}$ of $\mathrm{B}\mathrm{A}\mathrm{C}$ corresponding to the minimal theory such that if $\mathcal{M}$ is a model of ${\mathrm{B}\mathrm{A}\mathrm{C}}^{+}$, then $\langle M, $\mathcal{S}$^$\mathcal{M}$, \subseteq^$\mathcal{M}$ \rangle$isamodelof$$\mathrm{I}\mathrm{A}\mathrm{B}\mathrm{A}$_{$\mathrm{I}\mathrm{d}\mathrm{e}\mathrm{a}\mathrm{l}$}$, where ${\mathcal{S}}^{\mathcal{M}}$ is a unary predicate that distinguishes sets from classes. This is used to show that ${\mathrm{B}\mathrm{A}\mathrm{C}}^{+}$, a subsystem of $\mathrm{N}\mathrm{B}\mathrm{G}$, decides every $2$-sentence in the language of class theory that includes a unary predicate distinguishing sets from classes.