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