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

now :: thesis: for t being finite Tree st t in rng <*T1,T2*> holds
height t <= max ((height T1),(height T2))

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, A2, A3, A4, Th79; :: thesis: verum