let G be finite _Graph; :: thesis: for m, n being Nat
for x being Vertex of G st n in (((LexBFS:CSeq G) . m) `2 ) . x holds
ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) = y & not y in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) & x in G .AdjacentSet {y} )
let m, n be Nat; :: thesis: for x being Vertex of G st n in (((LexBFS:CSeq G) . m) `2 ) . x holds
ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) = y & not y in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) & x in G .AdjacentSet {y} )
set CS = LexBFS:CSeq G;
set CSM = (LexBFS:CSeq G) . m;
set V2M = ((LexBFS:CSeq G) . m) `2 ;
set CSN = (LexBFS:CSeq G) . ((G .order() ) -' n);
set VLN = ((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ;
set V2N = ((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ;
set on1 = ((G .order() ) -' n) + 1;
set CN1 = (LexBFS:CSeq G) . (((G .order() ) -' n) + 1);
set V21 = ((LexBFS:CSeq G) . (((G .order() ) -' n) + 1)) `2 ;
let x be Vertex of G; :: thesis: ( n in (((LexBFS:CSeq G) . m) `2 ) . x implies ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) = y & not y in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) & x in G .AdjacentSet {y} ) )
assume A1: n in (((LexBFS:CSeq G) . m) `2 ) . x ; :: thesis: ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) = y & not y in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) & x in G .AdjacentSet {y} )
A2: (((LexBFS:CSeq G) . m) `2 ) . x c= (Seg (G .order() )) \ (Seg ((G .order() ) -' m)) by Th43;
then A3: (G .order() ) -' m < n by A1, Th3;
n <= G .order() by A1, A2, Th3;
then A4: (G .order() ) -' n = (G .order() ) - n by XREAL_1:235;
then A5: (G .order() ) -' n < G .order() by A3, XREAL_1:46;
then A6: (G .order() ) -' ((G .order() ) -' n) = (G .order() ) - ((G .order() ) - n) by A4, XREAL_1:235;
then consider w being Vertex of G such that
A7: w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) and
A8: for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) implies (((LexBFS:CSeq G) . (((G .order() ) -' n) + 1)) `2 ) . v = ((((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . v) \/ {n} ) & ( ( not v in G .AdjacentSet {w} or v in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) ) implies (((LexBFS:CSeq G) . (((G .order() ) -' n) + 1)) `2 ) . v = (((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . v ) ) by A3, A4, Th42, XREAL_1:46;
(((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . x c= (Seg (G .order() )) \ (Seg ((G .order() ) -' ((G .order() ) -' n))) by Th43;
then A9: not n in (((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . x by A6, Th3;

A10: now

per cases ( m <= G .order() or G .order() < m ) ;

suppose m <= G .order() ; :: thesis: ((G .order() ) -' n) + 1 <= m

then (G .order() ) -' m = (G .order() ) - m by XREAL_1:235;
then ((G .order() ) - m) + m < n + m by A3, XREAL_1:8;
then (G .order() ) - n < (m + n) - n by XREAL_1:11;
hence ((G .order() ) -' n) + 1 <= m by A4, NAT_1:13; :: thesis: verum

end;

suppose G .order() < m ; :: thesis: ((G .order() ) -' n) + 1 <= m

then (G .order() ) -' n < m by A5, XXREAL_0:2;
hence ((G .order() ) -' n) + 1 <= m by NAT_1:13; :: thesis: verum

end;

end;

end;

A11: (G .order() ) -' n < ((G .order() ) -' n) + 1 by XREAL_1:41;
assume A12: for y being Vertex of G holds
( not LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) = y or y in dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) or not x in G .AdjacentSet {y} ) ; :: thesis: contradiction
dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) <> the_Vertices_of G by A5, Th36;
then not x in G .AdjacentSet {w} by A12, A7, Th30;
then not n in (((LexBFS:CSeq G) . (((G .order() ) -' n) + 1)) `2 ) . x by A9, A8;
hence contradiction by A1, A6, A10, A11, Th47; :: thesis: verum