let R be good Ring; :: thesis: AddressPart (halt (SCM R)) = {}
thus AddressPart (halt (SCM R)) = [0 ,{} ] `2 by SCMRING2:30
.= {} by MCART_1:def 2 ; :: thesis: verum