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 Th134; :: thesis: verum