Theorem empty_set_is_least

Proof
01. 1 ⊢ x ∈ ∅, hypo.
02. 1 ⊢ x ∈ A, empty_efq 1.
03. ⊢ x ∈ ∅ → x ∈ A, subj_intro 2.
04. ⊢ ∀x. x ∈ ∅ → x ∈ A, uq_intro 3.
empty_set_is_least. ⊢ ∅ ⊆ A, incl_intro 4.

Dependencies
The given proof depends on three axioms:
comp, efq, eq_subst.