Proof of proveit.logic.sets.inclusion.transitivity_subset_subset_eq theorem

import sys
sys.path.append('..') # allows access to modules in parent theory
import proveit

%proving transitivity_subset_subset_eq

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
transitivity_subset_subset_eq:
(see dependencies)

transitivity_subset_subset_eq may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".