let R be good Ring; :: thesis: [0 ,{} ] is Instruction of (SCM R)
( [0 ,{} ] in SCM-Instr R & SCM-Instr R = the Instructions of (SCM R) ) by Def1, Th2;
hence [0 ,{} ] is Instruction of (SCM R) ; :: thesis: verum