let G be _finite _Graph; 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; 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; ( 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
; 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;
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} )
; 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; verum