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 AFINSQ_1:24;
then A1: dom I c= dom (stop I) ;
assume loc in dom I ; :: thesis: loc in dom (stop I)
hence loc in dom (stop I) by A1; :: thesis: verum