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, l1 being Element of NAT holds not l in dom (Start-At (l1,S))
let S be non empty IC-Ins-separated realistic COM-Struct of N; :: thesis: for l, l1 being Element of NAT holds not l in dom (Start-At (l1,S))
let l, l1 be Element of NAT ; :: thesis: not l in dom (Start-At (l1,S))
assume l in dom (Start-At (l1,S)) ; :: thesis: contradiction
then NAT meets dom (Start-At (l1,S)) by XBOOLE_0:3;
hence contradiction by Th26; :: thesis: verum