incl_contraposition

Theorem incl_contraposition_compl

Theorem. incl_contraposition_compl
A ⊆ B → compl B ⊆ compl A

Proof
01. 1 ⊢ A ⊆ B, hypo.
02. 1 ⊢ UnivCl \ B ⊆ UnivCl \ A, incl_contraposition 1.
03. ⊢ compl A = UnivCl \ A, compl_as_diff.
04. ⊢ compl B = UnivCl \ B, compl_as_diff.
05. 1 ⊢ compl B ⊆ UnivCl \ A,
  eq_subst_rev 4 2, P t ↔ t ⊆ UnivCl \ A.
06. 1 ⊢ compl B ⊆ compl A,
  eq_subst_rev 3 5, P t ↔ compl B ⊆ t.
incl_contraposition_compl. ⊢ A ⊆ B → compl B ⊆ compl A,
  subj_intro 6.

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