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 = {}
A: dom (Start-At (k,S)) = {(IC S)} by FUNCOP_1:19;
not IC S in NAT by Def21;
then dom (Start-At (k,S)) misses NAT by A, ZFMISC_1:56;
hence (Start-At (k,S)) | NAT = {} by RELAT_1:95; :: thesis: verum