( d in SCM+FSA-Data-Loc & e in SCM+FSA-Data-Loc & f in SCM+FSA-Data-Loc & g in SCM+FSA-Data-Loc ) by SCMFSA_2:def 4;
hence {d,e,f,g} is Subset of Int-Locations by SUBSET_1:58; :: thesis: verum