theorem Th26: :: LEXBFS:26

for G being _finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st x in dom (L `1) holds
((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x