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)}) ;

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 ;

(((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' k)}) . x = {((G .order()) -' k)} by A3, FUNCOP_1:7;

hence ((LexBFS:Update (L,v,k)) `2) . x = ((L `2) . x) \/ {((G .order()) -' k)} by A4, Def1; :: thesis: verum

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)}) ;

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 ;

(((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' k)}) . x = {((G .order()) -' k)} by A3, FUNCOP_1:7;

hence ((LexBFS:Update (L,v,k)) `2) . x = ((L `2) . x) \/ {((G .order()) -' k)} by A4, Def1; :: thesis: verum