let G be _finite _Graph; :: thesis: for n being Nat holds
( dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )
let n be Nat; :: thesis: ( dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )
set VLN = ((MCS:CSeq G) . n) `1 ;
set CSO = (MCS:CSeq G) . (G .order());
set VLO = ((MCS:CSeq G) . (G .order())) `1 ;
thus ( dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G implies not n < G .order() ) by Th65; :: thesis: ( G .order() <= n implies dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G )
card (dom (((MCS:CSeq G) . (G .order())) `1)) = card (the_Vertices_of G) by Th65;
then A1: dom (((MCS:CSeq G) . (G .order())) `1) = the_Vertices_of G by CARD_2:102;
assume G .order() <= n ; :: thesis: dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G
hence dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G by A1, Th67; :: thesis: verum