th1
transitivity of inclusion in power set

-for_all(A, transitive(inc, powerset(A))).


********************************************************************************
theorem to be proved 

-for_all(A, transitive(inc, powerset(A))).
 
0 new conclusion 
-for_all(A, transitive(inc, powerset(A))).
 
0 add link inc 
0 add link transitive 
0 add link powerset 

active rules:elifon stop1 stop2 stop3 stop4 equal equaldef or1 or23 or4 or5 not hypnon hypnonnon hypnonimp hypimp not_or_1 not_or_2 hypequ hypnonequ concl_or_and => <=> for_all1 for_all2 only .. ..1 ilec1 ilec2 ilec3 ilec4 ilec5 ilec1a ilec1b and_trivial_1 and_trivial_2 stop_trivial stop_trivial_or conclet inc transitive transitive1 powerset powerset1 and defconcl1 defconcl1a defconcl1b defconcl1bb exists or defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 

0 new conclusion 
-for_all(A, only(powerset(A):B, transitive(inc, B))).
 
--------------------------------------------------------- rule elifon 
0 add object x 
0 new conclusion 
-only(powerset(x):A, transitive(inc, A)).
 
--------------------------------------------------------- rule for_all1 
0 add object powerset_x 
0 add hypothesis powerset(x):powerset_x 
0 new conclusion transitive(inc, powerset_x) 
--------------------------------------------------------- rule only 
0 add object inc 
0 definition of the conclusion 
0 new conclusion 
-for_all(A elt powerset_x, for_all(B elt powerset_x, for_all(C elt powerset_x, ..[inc, A, B]and..[inc, B, C]=> ..[inc, A, C]))).
 
--------------------------------------------------------- rule defconcl1 
0 add object x1 
0 add hypothesis x1 elt powerset_x 
0 new conclusion 
-for_all(A elt powerset_x, for_all(B elt powerset_x, ..[inc, x1, A]and..[inc, A, B]=> ..[inc, x1, B])).
 
--------------------------------------------------------- rule for_all2 
0 add object x2 
0 add hypothesis x2 elt powerset_x 
0 new conclusion 
-for_all(A elt powerset_x, ..[inc, x1, x2]and..[inc, x2, A]=> ..[inc, x1, A]).
 
--------------------------------------------------------- rule for_all2 
0 add object x3 
0 add hypothesis x3 elt powerset_x 
0 new conclusion ..[inc, x1, x2]and..[inc, x2, x3]=> ..[inc, x1, x3] 
--------------------------------------------------------- rule for_all2 
0 add hypothesis x1 inc x2 
0 add hypothesis x2 inc x3 
0 new conclusion ..[inc, x1, x3] 
--------------------------------------------------------- rule => 
0 new conclusion x1 inc x3 
--------------------------------------------------------- rule .. 
0 add hypothesis x1 inc x 
--------------------------------------------------------- rule powerset 
0 add hypothesis x2 inc x 
--------------------------------------------------------- rule powerset 
0 add hypothesis x3 inc x 
--------------------------------------------------------- rule powerset 
0 definition of the conclusion 
0 new conclusion 
-for_all(A, A elt x1=>A elt x3).
 
--------------------------------------------------------- rule defconcl1 
0 add object x4 
0 new conclusion x4 elt x1=>x4 elt x3 
--------------------------------------------------------- rule for_all1 
0 add hypothesis x4 elt x1 
0 new conclusion x4 elt x3 
--------------------------------------------------------- rule => 
0 add hypothesis x4 elt x2 
--------------------------------------------------------- rule inc 
0 add hypothesis x4 elt x3 
--------------------------------------------------------- rule inc 
0 new conclusion true 
--------------------------------------------------------- rule stop1 
theorem 0 proved in 0.89 seconds
================================================================================