let k be Integer; :: thesis: k in (union {INT}) \/ SCM-Memory
union {INT} = INT by ZFMISC_1:25;
then ( k in INT & INT c= (union {INT}) \/ SCM-Memory ) by INT_1:def 2, XBOOLE_1:7;
hence k in (union {INT}) \/ SCM-Memory ; :: thesis: verum