let k be Nat; :: thesis: [1,k] in SCM-Data-Loc
( 1 in {1} & k in NAT ) by ORDINAL1:def 12, TARSKI:def 1;
hence [1,k] in SCM-Data-Loc by ZFMISC_1:87; :: thesis: verum