let G be finite _Graph; :: thesis: for n being Nat st n < G .order() holds
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 ) ) ) )
let n be Nat; :: thesis: ( n < G .order() implies 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 ) ) ) ) )
assume A1: n < G .order() ; :: thesis: 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 ) ) ) )
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 CN1 = (LexBFS:CSeq G) . (n + 1);
set V21 = ((LexBFS:CSeq G) . (n + 1)) `2 ;
set w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n);
set k = (G .order() ) -' n;
A2: card (dom (((LexBFS:CSeq G) . n) `1 )) = n by A1, Th46;
(LexBFS:CSeq G) . (n + 1) = LexBFS:Step ((LexBFS:CSeq G) . n) by Def33;
then A4: (LexBFS:CSeq G) . (n + 1) = LexBFS:Update ((LexBFS:CSeq G) . n),(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)),n by A1, A2, Def32;
set VLv = (((LexBFS:CSeq G) . n) `1 ) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order() ) -' n));

A13: now

let v be set ; :: thesis: ( ( not v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} or v in dom (((LexBFS:CSeq G) . n) `1 ) ) implies (((LexBFS:CSeq G) . (n + 1)) `2 ) . b₁ = (((LexBFS:CSeq G) . n) `2 ) . b<sub>1</sub> )
assume A14: ( not v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} or v in dom (((LexBFS:CSeq G) . n) `1 ) ) ; :: thesis: (((LexBFS:CSeq G) . (n + 1)) `2 ) . b<sub>1</sub> = (((LexBFS:CSeq G) . n) `2 ) . b₁

per cases ( not v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} or v in dom (((LexBFS:CSeq G) . n) `1 ) ) by A14;

suppose not v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} ; :: thesis: (((LexBFS:CSeq G) . (n + 1)) `2 ) . b<sub>1</sub> = (((LexBFS:CSeq G) . n) `2 ) . b₁

hence (((LexBFS:CSeq G) . (n + 1)) `2 ) . v = (((LexBFS:CSeq G) . n) `2 ) . v by A4, Th32u; :: thesis: verum

end;

suppose v in dom (((LexBFS:CSeq G) . n) `1 ) ; :: thesis: (((LexBFS:CSeq G) . (n + 1)) `2 ) . b₁ = (((LexBFS:CSeq G) . n) `2 ) . b₁

hence (((LexBFS:CSeq G) . (n + 1)) `2 ) . v = (((LexBFS:CSeq G) . n) `2 ) . v by A4, Th33u; :: thesis: verum

end;

end;

end;

take LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) ; :: thesis: ( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} & 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 {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} or v in dom (((LexBFS:CSeq G) . n) `1 ) ) implies (((LexBFS:CSeq G) . (n + 1)) `2 ) . v = (((LexBFS:CSeq G) . n) `2 ) . v ) ) ) )
thus ( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} & 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 {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} or v in dom (((LexBFS:CSeq G) . n) `1 ) ) implies (((LexBFS:CSeq G) . (n + 1)) `2 ) . v = (((LexBFS:CSeq G) . n) `2 ) . v ) ) ) ) by A4, Th34u, A13; :: thesis: verum