let d be Data-Location ; :: thesis: d in Data-Locations SCM
d in SCM-Data-Loc by Def2;
hence d in Data-Locations SCM by Th72; :: thesis: verum