let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
loc in dom (stop I)
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies loc in dom (stop I) )
dom I c= dom (I ';' (Stop SCMPDS )) by SCMPDS_4:39;
then A1: dom I c= dom (stop I) by SCMPDS_4:def 7;
assume loc in dom I ; :: thesis: loc in dom (stop I)
hence loc in dom (stop I) by A1; :: thesis: verum