Theorem Intersection_is_lower_bound

States that ⋂M is a lower bound of M with respect to the inclusion order. See Union_is_upper_bound for the dual statement.

Proof
01. 1 ⊢ A = ⋂M, hypo.
02. 2 ⊢ B ∈ M, hypo.
03. 3 ⊢ x ∈ A, hypo.
04. 1, 3 ⊢ x ∈ ⋂M, eq_subst 1 3, P u ↔ x ∈ u.
05. 1, 2, 3 ⊢ x ∈ B, Intersection_elim 4 2.
06. 1, 2 ⊢ x ∈ A → x ∈ B, subj_intro 5.
07. 1, 2 ⊢ ∀x. x ∈ A → x ∈ B, uq_intro 6.
08. 1, 2 ⊢ A ⊆ B, incl_intro 7.
Intersection_is_lower_bound. ⊢ A = ⋂M → B ∈ M → A ⊆ B, subj_intro_ii 8.

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