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

import proveit
from proveit import x, y, A, B, C, fx, Px
from proveit.logic import And, Equals, Forall, InSet, NotSubsetEq, SubsetEq
from proveit.logic.equality  import substitution
from proveit.logic.equality import sub_right_side_into
from proveit.logic.sets.inclusion  import proper_subset_def, subset_eq_def
#from proveit.logic.sets.inclusion import relax_subset

%proving transitivity_subset_subset

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

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

proper_subset_def

 ⊢  

proper_subset_def_spec_a_b = proper_subset_def.instantiate()

proper_subset_def_spec_a_b:  ⊢  

# one possible way forward is to try to replace the improper subsets now with the definitions
# so how to take advantage of the def of improper subset shown below?
subset_eq_def

 ⊢  

subset_eq_def_spec_a_b = subset_eq_def.instantiate()

subset_eq_def_spec_a_b:  ⊢  

# # perhaps build it then prove it?
# try01 = Equals(ProperSubset(A, B), And(Forall(x, InSet(x, B), conditions=[InSet(x, A)]), NotSubsetEq(B, A)))

# sub_right_side_into_spec = sub_right_side_into.instantiate({Px:subset_def_spec_a_b, y:SubsetEq(A, B), x: Forall(x, InSet(x, B), conditions=[InSet(x, A)])}, assumptions=[subset_eq_def_spec_a_b.expr])

# sub_right_side_into_spec.prove()

# substitution

# substitution_spec = substitution.instantiate({fx:subset_def_spec_a_b, x:SubsetEq(A, B), y:Forall(x, InSet(x, B), conditions=[InSet(x, A)])})

# subset_def_spec_b_c = subset_def.instantiate({A:B, B:C})

# subset_def_spec_a_c = subset_def.instantiate({A:A, B:C})

# subset_eq_def_spec_a_b = subset_eq_def.instantiate({A:A, B:B})

# subset_eq_def_spec_b_c = subset_eq_def.instantiate({A:B, B:C})

# subset_eq_def_spec_a_c = subset_eq_def.instantiate({A:A, B:C})

# subset_def_spec_a_b_derived = subset_def_spec_a_b.derive_right_via_equality(ProperSubset(A, B)])

# subset_def_spec_b_c_derived = subset_def_spec_b_c.derive_right_via_equality(ProperSubset(B, C)])

# subset_def_spec_a_c.rhs.prove(assumptions=ProperSubset(A,B), ProperSubset(B,C)})

# subset_def_spec_a_b_derived.inner_expr()

# subset_eq_def_spec.sub_right_side_into(subset_def_spec_a_b_derived)

# subset_def_spec_b_c.derive_right_via_equality(ProperSubset(A, B), ProperSubset(B, C)])

# %qed