*******************************************************************************
Theoreme a demontrer

 ! [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) ) )

*******************************************************************************
Demonstration
            
SZS status Theorem for SET027+4.p

etapes utiles:[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 :

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

*** explication : theoreme initial
--------------------------------------------------------- action(ini)
creer objet(s) z3 z2 z1  
*** nouvconcl(0, subset(z1, z2)&subset(z2, z3)=>subset(z1, z3), 2) 

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

*** explication : on instancie la(les) variable(s) universelle(s) de la conclusion
--------------------------------------------------------- regle(!)
*** ajhyp(0, subset(z1, z2), 3)  
*** ajhyp(0, subset(z2, z3), 3) 
*** nouvconcl(0, subset(z1, z3), 3) 

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

*** explication : pour demontrer H=>C, on suppose H et on doit demontrer C
--------------------------------------------------------- regle(=>)
*** nouvconcl(0, ![A]: (member(A, z1)=>member(A, z3)), 4) 

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

*** explication : on remplace la conclusion  subset(z1, z3)  par sa definition(fof subset ) 
--------------------------------------------------------- regle(def_concl_pred)
creer objet(s) z4  
*** nouvconcl(0, member(z4, z1)=>member(z4, z3), 5) 

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

*** explication : on instancie la(les) variable(s) universelle(s) de la conclusion
--------------------------------------------------------- regle(!)
*** ajhyp(0, member(z4, z1), 6) 
*** nouvconcl(0, member(z4, z3), 6) 

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

*** explication : pour demontrer H=>C, on suppose H et on doit demontrer C
--------------------------------------------------------- regle(=>)
*** ajhyp(0, member(z4, z2), 7) 

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

*** explication : regle2 si (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))alors ajhyp(A, member(C, D), _) 
construite a partir de la definition de subset (fof subset ) 
--------------------------------------------------------- regle(subset)
*** ajhyp(0, member(z4, z3), 8) 

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

*** explication : regle2 si (hyp(A, subset(B, D), _), hyp(A, member(C, B), _), obj_cte(A, C))alors ajhyp(A, member(C, D), _) 
construite a partir de la definition de subset (fof subset ) 
--------------------------------------------------------- regle(subset)
*** nouvconcl(0, true, 9) 

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

*** explication : la conclusion member(z4, z3) a demontrer est une hypothese 
--------------------------------------------------------- regle(stop_hyp_concl)
le theoreme initial 0 est donc demontre
* * * * * * * * * * * * * * * * * * * * * * * *

SZS output end proof for SET027+4.p