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