let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being program-free PartState of S holds NPP p = p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being program-free PartState of S holds NPP p = p
let p be program-free PartState of S; :: thesis: NPP p = p
p | NAT = {} by Def29;
then ProgramPart p = {} ;
hence NPP p = p ; :: thesis: verum