let s be State of SCMPDS ; :: thesis: for l being Element of NAT holds dom (s | NAT ) misses dom (Start-At l,SCMPDS )
let l be Element of NAT ; :: thesis: dom (s | NAT ) misses dom (Start-At l,SCMPDS )

now

let x be set ; :: thesis: ( x in dom (s | NAT ) implies not x in dom (Start-At l,SCMPDS ) )
assume x in dom (s | NAT ) ; :: thesis: not x in dom (Start-At l,SCMPDS )
then x is Element of NAT by Th1;
then x is Element of NAT ;
then x <> IC SCMPDS by AMI_1:48;
then not x in {(IC SCMPDS )} by TARSKI:def 1;
hence not x in dom (Start-At l,SCMPDS ) by FUNCOP_1:19; :: thesis: verum

end;

hence dom (s | NAT ) misses dom (Start-At l,SCMPDS ) by XBOOLE_0:3; :: thesis: verum