let T be Tree; :: thesis: elementary_tree 1 c= ^ T
let x be set ; :: 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:47, TARSKI:def 2, TREES_1:47, TREES_1:88;
hence x in ^ T by Th63; :: thesis: verum