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