logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving superset_membership_from_proper_subset
Out[2]:
Under these presumptions, we begin our proof of
superset_membership_from_proper_subset:
(see dependencies)
In [3]:
A_propersub_B = superset_membership_from_proper_subset.condition
Out[3]:
A_propersub_B:
In [4]:
A_propersub_B__unfolded = A_propersub_B.unfold(assumptions=[A_propersub_B])
Out[4]:
A_propersub_B__unfolded:  ⊢  
In [5]:
A_sub_B = A_propersub_B__unfolded.derive_left()
Out[5]:
A_sub_B:  ⊢  
In [6]:
%qed
Out[6]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3, 4,  ⊢  
  : , : , :
2theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
3instantiation5, 6  ⊢  
  : , :
4assumption  ⊢  
5theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
6instantiation7, 8  ⊢  
  : , :
7theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_proper_subset
8assumption  ⊢