let N be with_non-empty_elements set ; :: thesis: for S being non empty COM-Struct of N
for p being data-only PartState of S holds ProgramPart p = {}
let S be non empty COM-Struct of N; :: thesis: for p being data-only PartState of S holds ProgramPart p = {}
let p be data-only PartState of S; :: thesis: ProgramPart p = {}
dom p misses {(IC S)} \/ NAT by Def50;
then dom p misses NAT by XBOOLE_1:70;
hence ProgramPart p = {} by RELAT_1:187; :: thesis: verum