*******************************************************************************
Theorem to be proved

 ! [A,B,C] : ( ( subset(A,B) & subset(B,C) ) => subset(A,C) ) )

*******************************************************************************
Definition

! [A,B] : ( subset(A,B) <=> ! [X] : ( member(X,A) => member(X,B) ) ) 
            
*******************************************************************************
Proof

SZS status Theorem for SET027+4.p

useful steps:[1, 2, 3, 4, 5, 6, 7, 8, 9]
SZS output start proof for SET027+4.p

* * * * * * * * * * * * * * * * * * * * * * * *
in the following, N is the number of a (sub)theorem
                  E is the current step
hyp(N,H,E) means that H is an hypothesis of (sub)theorem N
concl(N,C,E) means that C is the conclusion of (sub)theorem N
obj_cte(N,C) means that C is a created object or a given constant
addhyp(N,H,E) means add H as a new hypothesis for N
newconcl(N,C,E) means that the new conclusion of N is C
           (C replaces the precedent conclusion)
a subtheorem N0-i or N0+i is a subtheorem of the (sub)theorem N0
   N0 is proved if all N0-i have been proved (&-node)
             or if one N0+i have been proved (|-node)
the initial theorem is numbered 0

* * * theorem to be proved
![A, B, C]: (subset(A, B)&subset(B, C)=>subset(A, C))

* * * proof :

* * * * * * theorem 0 * * * * * *
*** newconcl(0, ![A, B, C]: (subset(A, B)&subset(B, C)=>subset(A, C)), 1) 

*** explanation : initial theorem
--------------------------------------------------------- action(ini)
create object(s) z3 z2 z1  
*** newconcl(0, subset(z1, z2)&subset(z2, z3)=>subset(z1, z3), 2) 

*** because concl((0, ![A, B, C]: (subset(A, B)&subset(B, C)=>subset(A, C))), 1) 

*** explanation : the variables of the conclusion are instantiated
--------------------------------------------------------- rule(!)
*** addhyp(0, subset(z1, z2), 3)  
*** addhyp(0, subset(z2, z3), 3) 
*** newconcl(0, subset(z1, z3), 3) 

*** because concl(0, subset(z1, z2)&subset(z2, z3)=>subset(z1, z3), 2) 

*** explanation : to prove H=>C, assume H and prove C
--------------------------------------------------------- rule(=>)
*** newconcl(0, ![A]: (member(A, z1)=>member(A, z3)), 4) 

*** because concl(0, subset(z1, z3), 3) 

*** explanation : the conclusion  subset(z1, z3) is replaced by its definition(fof subset ) 
--------------------------------------------------------- rule(def_concl_pred)
create object(s) z4  
*** newconcl(0, member(z4, z1)=>member(z4, z3), 5) 

*** because concl((0, ![A]: (member(A, z1)=>member(A, z3))), 4) 

*** explanation : the variables of the conclusion are instantiated
--------------------------------------------------------- rule(!)
*** addhyp(0, member(z4, z1), 6) 
*** newconcl(0, member(z4, z3), 6) 

*** because concl(0, member(z4, z1)=>member(z4, z3), 5) 

*** explanation : to prove H=>C, assume H and prove C
--------------------------------------------------------- rule(=>)
*** addhyp(0, member(z4, z2), 7) 

*** because hyp(0, subset(z1, z2), 3), hyp(0, member(z4, z1), 6), obj_cte(0, z4) 

*** explanation : rule2 if (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))then addhyp(A, member(C, D), _) 
built from the definition of subset (fof subset ) 
--------------------------------------------------------- rule(subset)
*** addhyp(0, member(z4, z3), 8) 

*** because hyp(0, subset(z2, z3), 3), hyp(0, member(z4, z2), 7), obj_cte(0, z4) 

*** explanation : rule2 if (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))then addhyp(A, member(C, D), _) 
built from the definition of subset (fof subset ) 
--------------------------------------------------------- rule(subset)
*** newconcl(0, true, 9) 

*** because hyp(0, member(z4, z3), 8), concl(0, member(z4, z3), 6) 

*** explanation : the conclusion member(z4, z3) to be proved is a hypothesis 
--------------------------------------------------------- rule(stop_hyp_concl)
then the initial theorem is proved
* * * * * * * * * * * * * * * * * * * * * * * *

SZS output end proof for SET027+4.p