let k be Element of SCM-Memory ; :: thesis: ( k = NAT or k in SCM-Data-Loc )
k in {NAT} \/ SCM-Data-Loc by XBOOLE_0:def 3;
then ( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def 3;
hence ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def 1; :: thesis: verum