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 CSN = (LexBFS:CSeq G) . n;
set VLN = ((LexBFS:CSeq G) . n) `1 ;
set V2N = ((LexBFS:CSeq G) . n) `2 ;
set CSM = (LexBFS:CSeq G) . m;
set V2M = ((LexBFS:CSeq G) . m) `2 ;
assume that
A3: y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) and
A4: not x in dom (((LexBFS:CSeq G) . n) `1 ) and
A5: x in G .AdjacentSet {y} ; :: thesis: (G .order() ) -' n in (((LexBFS:CSeq G) . m) `2 ) . x
set CN1 = (LexBFS:CSeq G) . (n + 1);
set V21 = ((LexBFS:CSeq G) . (n + 1)) `2 ;
consider w being Vertex of G such that
A6: w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) and
A7: 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, Th54;
A8: (((LexBFS:CSeq G) . (n + 1)) `2 ) . x = ((((LexBFS:CSeq G) . n) `2 ) . x) \/ {((G .order() ) -' n)} by A3, A4, A5, A6, A7;
(G .order() ) -' n in {((G .order() ) -' n)} by TARSKI:def 1;
then A9: (G .order() ) -' n in (((LexBFS:CSeq G) . (n + 1)) `2 ) . x by A8, XBOOLE_0:def 3;
n + 1 <= m by A2, NAT_1:13;
then (((LexBFS:CSeq G) . (n + 1)) `2 ) . x c= (((LexBFS:CSeq G) . m) `2 ) . x by Th56;
hence (G .order() ) -' n in (((LexBFS:CSeq G) . m) `2 ) . x by A9; :: thesis: verum