:: deftheorem defines nodic JGRAPH_1:def 4 :
for n being Nat
for IT being FinSequence of (TOP-REAL n) holds
( IT is nodic iff for i, j being Nat holds
( not LSeg (IT,i) meets LSeg (IT,j) or ( (LSeg (IT,i)) /\ (LSeg (IT,j)) = {(IT . i)} & ( IT . i = IT . j or IT . i = IT . (j + 1) ) ) or ( (LSeg (IT,i)) /\ (LSeg (IT,j)) = {(IT . (i + 1))} & ( IT . (i + 1) = IT . j or IT . (i + 1) = IT . (j + 1) ) ) or LSeg (IT,i) = LSeg (IT,j) ) );