Theorem incl_from_eq_rev

Proof
01. 1 ⊢ A = B, hypo.
02. ⊢ A ⊆ A, incl_refl.
03. 1 ⊢ B ⊆ A, eq_subst 1 2, P X ↔ X ⊆ A.
incl_from_eq_rev. ⊢ A = B → B ⊆ A, subj_intro 3.

Dependencies
The given proof depends on one axiom:
eq_subst.