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

import proveit
from proveit.logic.sets.inclusion  import proper_subset_def
theory = proveit.Theory() # the theorem's theory

%proving relax_proper_subset

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

# pull in the axiomatic definition of proper subset
proper_subset_def

 ⊢  

proper_subset_def_inst = proper_subset_def.instantiate()

proper_subset_def_inst:  ⊢  

proper_subset_def_inst.derive_right_via_equality(assumptions=[proper_subset_def_inst.lhs])

 ⊢  

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

%qed

proveit.logic.sets.inclusion.relax_proper_subset has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
3	instantiation	4, 5, 6	⊢
	: , :
4	theorem		⊢
	proveit.logic.equality.rhs_via_equality
5	assumption		⊢
6	instantiation	7	⊢
	: , :
7	axiom		⊢
	proveit.logic.sets.inclusion.proper_subset_def