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 l being Element of NAT holds dom (Start-At l,S) misses NAT
let S be non empty IC-Ins-separated realistic COM-Struct of N; :: thesis: for l being Element of NAT holds dom (Start-At l,S) misses NAT
let l be Element of NAT ; :: thesis: dom (Start-At l,S) misses NAT
( dom (Start-At l,S) = {(IC S)} & not IC S in NAT ) by Def21, FUNCOP_1:19;
hence dom (Start-At l,S) misses NAT by ZFMISC_1:56; :: thesis: verum