let k be Integer; :: thesis: k in SCM-Data-Loc \/ INT
( k in INT & INT c= SCM-Data-Loc \/ INT ) by INT_1:def 2, XBOOLE_1:7;
hence k in SCM-Data-Loc \/ INT ; :: thesis: verum