let T1, T2, W1, W2 be Tree; :: thesis: ( tree (T1,T2) = tree (W1,W2) implies ( T1 = W1 & T2 = W2 ) )
assume A1: tree (T1,T2) = tree (W1,W2) ; :: thesis: ( T1 = W1 & T2 = W2 )

now :: thesis: for p being FinSequence holds
( p in T1 iff p in W1 )

let p be FinSequence; :: thesis: ( p in T1 iff p in W1 )
( p in T1 iff <*0*> ^ p in tree (T1,T2) ) by Th69;
hence ( p in T1 iff p in W1 ) by A1, Th69; :: thesis: verum

end;

hence for p being FinSequence of NAT holds
( p in T1 iff p in W1 ) ; :: according to TREES_2:def 1 :: thesis: T2 = W2
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in T2 or p in W2 ) & ( not p in W2 or p in T2 ) )
( p in T2 iff <*1*> ^ p in tree (T1,T2) ) by Th70;
hence ( ( not p in T2 or p in W2 ) & ( not p in W2 or p in T2 ) ) by A1, Th70; :: thesis: verum