let G be _finite _Graph; :: thesis: for x being set
for i, j being Nat st i <= j holds
(((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x
let x be set ; :: thesis: for i, j being Nat st i <= j holds
(((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x
let i, j be Nat; :: thesis: ( i <= j implies (((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x )
assume i <= j ; :: thesis: (((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x
then A1: ex k being Nat st j = i + k by NAT_1:10;
set CS = LexBFS:CSeq G;
set CSI = (LexBFS:CSeq G) . i;
set V2I = ((LexBFS:CSeq G) . i) `2 ;
defpred S<sub>1</sub>[ Nat] means (((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . (i + $1)) `2) . x;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set CK1 = (LexBFS:CSeq G) . ((i + k) + 1);
set CSK = (LexBFS:CSeq G) . (i + k);
set V2K = ((LexBFS:CSeq G) . (i + k)) `2 ;
set VLK = ((LexBFS:CSeq G) . (i + k)) `1 ;
set V21 = ((LexBFS:CSeq G) . ((i + k) + 1)) `2 ;

per cases ( (i + k) + 1 <= G .order() or G .order() < (i + k) + 1 ) ;

suppose (i + k) + 1 <= G .order() ; :: thesis: S₁[k + 1]

then i + k < G .order() by NAT_1:13;
then consider w being Vertex of G such that
w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . (i + k)) and
A4: for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . (i + k)) `1) implies (((LexBFS:CSeq G) . ((i + k) + 1)) `2) . v = ((((LexBFS:CSeq G) . (i + k)) `2) . v) \/ {((G .order()) -' (i + k))} ) & ( ( not v in G .AdjacentSet {w} or v in dom (((LexBFS:CSeq G) . (i + k)) `1) ) implies (((LexBFS:CSeq G) . ((i + k) + 1)) `2) . v = (((LexBFS:CSeq G) . (i + k)) `2) . v ) ) by Th42;

per cases ( ( x in G .AdjacentSet {w} & not x in dom (((LexBFS:CSeq G) . (i + k)) `1) ) or not x in G .AdjacentSet {w} or x in dom (((LexBFS:CSeq G) . (i + k)) `1) ) ;

suppose ( x in G .AdjacentSet {w} & not x in dom (((LexBFS:CSeq G) . (i + k)) `1) ) ; :: thesis: S₁[k + 1]

then (((LexBFS:CSeq G) . ((i + k) + 1)) `2) . x = ((((LexBFS:CSeq G) . (i + k)) `2) . x) \/ {((G .order()) -' (i + k))} by A4;
then (((LexBFS:CSeq G) . (i + k)) `2) . x c= (((LexBFS:CSeq G) . ((i + k) + 1)) `2) . x by XBOOLE_1:7;
hence S₁[k + 1] by A3, XBOOLE_1:1; :: thesis: verum

end;

suppose ( not x in G .AdjacentSet {w} or x in dom (((LexBFS:CSeq G) . (i + k)) `1) ) ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by A3, A4; :: thesis: verum

end;

end;

end;

suppose A5: G .order() < (i + k) + 1 ; :: thesis: S₁[k + 1]

A6: i + k <= (i + k) + 1 by NAT_1:13;
G .order() <= i + k by A5, NAT_1:13;
hence S₁[k + 1] by A3, A6, Th34; :: thesis: verum

end;

end;

end;

A7: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A2);
hence (((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x by A1; :: thesis: verum