let G be _finite _Graph; :: thesis: for m, n being Nat
for x, y being set st n < G .order() & n < m & y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & not x in dom (((LexBFS:CSeq G) . n) `1) & x in G .AdjacentSet {y} holds
(G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x
let m, n be Nat; :: thesis: for x, y being set st n < G .order() & n < m & y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & not x in dom (((LexBFS:CSeq G) . n) `1) & x in G .AdjacentSet {y} holds
(G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x
let x, y be set ; :: thesis: ( n < G .order() & n < m & y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & not x in dom (((LexBFS:CSeq G) . n) `1) & x in G .AdjacentSet {y} implies (G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x )
assume that
A1: n < G .order() and
A2: n < m ; :: thesis: ( not y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) or x in dom (((LexBFS:CSeq G) . n) `1) or not x in G .AdjacentSet {y} or (G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x )
set CS = LexBFS:CSeq G;
set CSM = (LexBFS:CSeq G) . m;
set V2M = ((LexBFS:CSeq G) . m) `2 ;
set CN1 = (LexBFS:CSeq G) . (n + 1);
set V21 = ((LexBFS:CSeq G) . (n + 1)) `2 ;
n + 1 <= m by A2, NAT_1:13;
then A3: (((LexBFS:CSeq G) . (n + 1)) `2) . x c= (((LexBFS:CSeq G) . m) `2) . x by Th44;
A4: (G .order()) -' n in {((G .order()) -' n)} by TARSKI:def 1;
set CSN = (LexBFS:CSeq G) . n;
set VLN = ((LexBFS:CSeq G) . n) `1 ;
set V2N = ((LexBFS:CSeq G) . n) `2 ;
assume that
A5: y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) and
A6: not x in dom (((LexBFS:CSeq G) . n) `1) and
A7: x in G .AdjacentSet {y} ; :: thesis: (G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x
ex w being Vertex of G st
( w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . n) `1) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = ((((LexBFS:CSeq G) . n) `2) . v) \/ {((G .order()) -' n)} ) & ( ( not v in G .AdjacentSet {w} or v in dom (((LexBFS:CSeq G) . n) `1) ) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = (((LexBFS:CSeq G) . n) `2) . v ) ) ) ) by A1, Th42;
then (((LexBFS:CSeq G) . (n + 1)) `2) . x = ((((LexBFS:CSeq G) . n) `2) . x) \/ {((G .order()) -' n)} by A5, A6, A7;
then (G .order()) -' n in (((LexBFS:CSeq G) . (n + 1)) `2) . x by A4, XBOOLE_0:def 3;
hence (G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x by A3; :: thesis: verum