let T be Tree; :: thesis: elementary_tree 1 c= ^ T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in elementary_tree 1 or x in ^ T )
assume x in elementary_tree 1 ; :: thesis: x in ^ T
then reconsider p = x as Element of elementary_tree 1 ;
( p = {} or ( p = <*0*> & {} in T & <*0*> ^ {} = <*0*> ) ) by FINSEQ_1:34, TARSKI:def 2, TREES_1:22, TREES_1:51;
hence x in ^ T by Th60; :: thesis: verum