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

( 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