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