let t be Terminal of SCM-AE; :: thesis: max_Data-Loc_in (root-tree t) = d". t
max_Data-Loc_in (root-tree t) = f . (root-tree t) by Def14, Lm4, Lm5;
hence max_Data-Loc_in (root-tree t) = d". t by Lm4; :: thesis: verum