let T1, T2 be Tree; :: thesis: elementary_tree 2 c= tree T1,T2
let x be set ; :: 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:47, TREES_1:47, TREES_1:90;
hence x in tree T1,T2 by Th71; :: thesis: verum