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