let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty COM-Struct of N
for p being program-free PartState of S holds dom p misses NAT
let S be non empty COM-Struct of N; :: thesis: for p being program-free PartState of S holds dom p misses NAT
let p be program-free PartState of S; :: thesis: dom p misses NAT
p | NAT = {} by Def29;
hence dom p misses NAT by RELAT_1:95; :: thesis: verum