theorem :: TREES_3:73

for T1, T2, W1, W2 being Tree st tree (T1,T2) = tree (W1,W2) holds
( T1 = W1 & T2 = W2 )