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 A2: 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} )
assume A3: 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
(((LexBFS:CSeq G) . m) `2 ) . x c= (Seg (G .order() )) \ (Seg ((G .order() ) -' m)) by Th55;
then A4: ( (G .order() ) -' m < n & n <= G .order() ) by A2, Th5;
then A5: (G .order() ) -' n = (G .order() ) - n by XREAL_1:235;
then A6: (G .order() ) -' n < G .order() by A4, XREAL_1:46;
then A7: (G .order() ) -' ((G .order() ) -' n) = (G .order() ) - ((G .order() ) - n) by A5, XREAL_1:235;
(((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . x c= (Seg (G .order() )) \ (Seg ((G .order() ) -' ((G .order() ) -' n))) by Th55;
then A8: not n in (((LexBFS:CSeq G) . ((G .order() ) -' n)) `2 ) . x by A7, Th5;
consider w being Vertex of G such that
A9: w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' n)) and
A10: 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 A4, A5, A7, Th54, XREAL_1:46;
dom (((LexBFS:CSeq G) . ((G .order() ) -' n)) `1 ) <> the_Vertices_of G by A6, Th50;
then not x in G .AdjacentSet {w} by A3, A9, Th41;
then A11: not n in (((LexBFS:CSeq G) . (((G .order() ) -' n) + 1)) `2 ) . x by A8, A10;

A12: 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 A4, XREAL_1:8;
then (G .order() ) - n < (m + n) - n by XREAL_1:11;
hence ((G .order() ) -' n) + 1 <= m by A5, NAT_1:13; :: thesis: verum

end;

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

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

end;

end;

end;

(G .order() ) -' n < ((G .order() ) -' n) + 1 by XREAL_1:41;
hence contradiction by A2, A7, A11, A12, Th59; :: thesis: verum