let d be Element of SCM-Data-Loc ; :: thesis: d in SCM-Data-Loc \/ INT
SCM-Data-Loc c= SCM-Data-Loc \/ INT by XBOOLE_1:7;
hence d in SCM-Data-Loc \/ INT by TARSKI:def 3; :: thesis: verum