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