let G be finite _Graph; :: thesis: for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st x in G .AdjacentSet {v} & not x in dom (L `1 ) holds
((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)}
let L be LexBFS:Labeling of G; :: thesis: for v being Vertex of G
for x being set
for k being Nat st x in G .AdjacentSet {v} & not x in dom (L `1 ) holds
((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)}
let v be Vertex of G; :: thesis: for x being set
for k being Nat st x in G .AdjacentSet {v} & not x in dom (L `1 ) holds
((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)}
let x be set ; :: thesis: for k being Nat st x in G .AdjacentSet {v} & not x in dom (L `1 ) holds
((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)}
let k be Nat; :: thesis: ( x in G .AdjacentSet {v} & not x in dom (L `1 ) implies ((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)} )
assume that
A1: x in G .AdjacentSet {v} and
A2: not x in dom (L `1 ) ; :: thesis: ((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)}
A3: x in (G .AdjacentSet {v}) \ (dom (L `1 )) by A1, A2, XBOOLE_0:def 5;
then x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) by FUNCOP_1:19;
then A4: x in (dom (L `2 )) \/ (dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)})) by XBOOLE_0:def 3;
set L2 = (LexBFS:Update L,v,k) `2 ;
A5: (LexBFS:Update L,v,k) `2 = (L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) by MCART_1:7;
(((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) . x = {((G .order() ) -' k)} by A3, FUNCOP_1:13;
hence ((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ {((G .order() ) -' k)} by A5, A4, Def2; :: thesis: verum