let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (SCM-OK | NAT) or x in {SCM-Instr} )
assume x in rng (SCM-OK | NAT) ; :: thesis: x in {SCM-Instr}
then consider y being set such that
A1: y in dom (SCM-OK | NAT) and
A2: (SCM-OK | NAT) . y = x by FUNCT_1:def 5;
A3: y in NAT by A1, RELAT_1:86;
x = SCM-OK . y by A1, A2, FUNCT_1:70
.= SCM-Instr by A3, AMI_2:11 ;
hence x in {SCM-Instr} by TARSKI:def 1; :: thesis: verum