:: deftheorem Def13 defines LexBFS:Step LEXBFS:def 14 :
for G being _finite _Graph
for L being LexBFS:Labeling of G holds
( ( G .order() <= card (dom (L `1)) implies LexBFS:Step L = L ) & ( not G .order() <= card (dom (L `1)) implies LexBFS:Step L = LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1)))) ) );