Theorem Union_is_upper_bound

States that ⋃M is an upper bound of M with respect to the inclusion order. See Intersection_is_lower_bound for the dual statement.

Proof
01. 1 ⊢ A = ⋃M, hypo.
02. 2 ⊢ B ∈ M, hypo.
03. 3 ⊢ x ∈ B, hypo.
04. 2, 3 ⊢ x ∈ ⋃M, Union_intro 2 3.
05. 1, 2, 3 ⊢ x ∈ A, eq_subst_rev 1 4, P t ↔ x ∈ t.
06. 1, 2 ⊢ x ∈ B → x ∈ A, subj_intro 5.
07. 1, 2 ⊢ ∀x. x ∈ B → x ∈ A, uq_intro 6.
08. 1, 2 ⊢ B ⊆ A, incl_intro 7.
Union_is_upper_bound. ⊢ A = ⋃M → B ∈ M → B ⊆ A,
  subj_intro_ii 8.

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