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 Def13, Lm6, Lm7;
hence max_Data-Loc_in (root-tree t) = d". t by Lm6; :: thesis: verum