let T1, T2 be Tree; :: thesis: ( ^ T1 = ^ T2 implies T1 = T2 )
assume A1: ^ T1 = ^ T2 ; :: thesis: T1 = T2
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in T1 or p in T2 ) & ( not p in T2 or p in T1 ) )
( p in T1 iff <*0*> ^ p in ^ T1 ) by Th61;
hence ( ( not p in T1 or p in T2 ) & ( not p in T2 or p in T1 ) ) by A1, Th61; :: thesis: verum