let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic COM-Struct of N
for k being Element of NAT holds (Start-At (k,S)) | NAT = {}
let S be non empty IC-Ins-separated realistic COM-Struct of N; :: thesis: for k being Element of NAT holds (Start-At (k,S)) | NAT = {}
let k be Element of NAT ; :: thesis: (Start-At (k,S)) | NAT = {}
A1: dom (Start-At (k,S)) = {(IC )} by FUNCOP_1:19;
not IC in NAT by Def12;
then dom (Start-At (k,S)) misses NAT by A1, ZFMISC_1:56;
hence (Start-At (k,S)) | NAT = {} by RELAT_1:95; :: thesis: verum