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