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