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