for T1, T2 being Tree st ( for n being Nat holds T1 -level n = T2 -level n ) holds
T1 = T2