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