theorem Th5: :: SCMRINGI:5

for S being non empty 1-sorted holds SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]