theorem :: LEXBFS:78

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