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:233;
then A5: (G .order()) -' n < G .order() by A3, XREAL_1:44;
then A6: (G .order()) -' ((G .order()) -' n) = (G .order()) - ((G .order()) - n) by A4, XREAL_1:233;
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:44;
(((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 :: thesis: ((G .order()) -' n) + 1 <= m

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:233;
then ((G .order()) - m) + m < n + m by A3, XREAL_1:6;
then (G .order()) - n < (m + n) - n by XREAL_1:9;
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:39;
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