let T1, T2 be finite Tree; :: thesis: height (tree T1,T2) = (max (height T1),(height T2)) + 1
set m = max (height T1),(height T2);
( height T2 <= height T1 or height T2 > height T1 ) ;
then A1: ( tree T1,T2 = tree <*T1,T2*> & rng <*T1,T2*> = {T1,T2} & T1 in {T1,T2} & T2 in {T1,T2} & ( max (height T1),(height T2) = height T1 or max (height T1),(height T2) = height T2 ) ) by FINSEQ_2:147, TARSKI:def 2, XXREAL_0:def 10;

now

let t be finite Tree; :: thesis: ( t in rng <*T1,T2*> implies height t <= max (height T1),(height T2) )
assume t in rng <*T1,T2*> ; :: thesis: height t <= max (height T1),(height T2)
then ( t = T1 or t = T2 ) by A1, TARSKI:def 2;
hence height t <= max (height T1),(height T2) by XXREAL_0:25; :: thesis: verum

end;

hence height (tree T1,T2) = (max (height T1),(height T2)) + 1 by A1, Th82; :: thesis: verum