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