theorem Th17: :: LEXBFS:17

for G being _finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st m <= n holds
S . m c= S . n