for T0, T1 being Tree
for t being Element of tree (T0,T1) holds
( ( for p being Element of T0 st t = <*0*> ^ p holds
( t in Leaves (tree (T0,T1)) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) )