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