set x = the Element of SCM-Data-Loc ;
reconsider x = the Element of SCM-Data-Loc as Object of SCM ;
take x ; :: thesis: x in SCM-Data-Loc
thus x in SCM-Data-Loc ; :: thesis: verum