theorem Th40: :: LEXBFS:40

for G being _finite _Graph holds ((LexBFS:CSeq G) ``1) .Result() = ((LexBFS:CSeq G) .Result()) `1