theorem :: LEXBFS:77

for G being finite _Graph
for n being Nat holds ((MCS:CSeq G) . n) `1 is with_property_T