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