let G be _finite _Graph; :: thesis: for i being Nat
for v being set holds (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))
let i be Nat; :: thesis: for v being set holds (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))
let v be set ; :: thesis: (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))
set CS = LexBFS:CSeq G;
set CSI = (LexBFS:CSeq G) . i;
set V2I = ((LexBFS:CSeq G) . i) `2 ;
set CSO = (LexBFS:CSeq G) . (G .order());
set V2O = ((LexBFS:CSeq G) . (G .order())) `2 ;
defpred S<sub>1</sub>[ Nat] means ( $1 <= G .order() implies (((LexBFS:CSeq G) . $1) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' $1)) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

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

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

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

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

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

A6: ((Seg (G .order())) \ (Seg ((G .order()) -' k))) \/ {((G .order()) -' k)} = (Seg (G .order())) \ (Seg ((G .order()) -' (k + 1))) by A3, Th5;
(((LexBFS:CSeq G) . (k + 1)) `2) . v = ((((LexBFS:CSeq G) . k) `2) . v) \/ {((G .order()) -' k)} by A4, A5;
hence S₁[k + 1] by A2, A6, NAT_1:13, XBOOLE_1:9; :: thesis: verum

end;

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

k <= k + 1 by NAT_1:13;
then A8: (Seg (G .order())) \ (Seg ((G .order()) -' k)) c= (Seg (G .order())) \ (Seg ((G .order()) -' (k + 1))) by Th4;
(((LexBFS:CSeq G) . (k + 1)) `2) . v = (((LexBFS:CSeq G) . k) `2) . v by A4, A7;
hence S₁[k + 1] by A2, A8, NAT_1:13, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

(LexBFS:CSeq G) . 0 = LexBFS:Init G by Def16;
then (((LexBFS:CSeq G) . 0) `2) . v = {} ;
then A9: S₁[ 0 ] by XBOOLE_1:2;
A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A1);

per cases ( i <= G .order() or i > G .order() ) ;

suppose i <= G .order() ; :: thesis: (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))

hence (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i)) by A10; :: thesis: verum

end;

suppose A11: i > G .order() ; :: thesis: (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))

then (G .order()) - i < i - i by XREAL_1:9;
then (G .order()) -' i = 0 by XREAL_0:def 2;
then A12: (G .order()) -' (G .order()) = (G .order()) -' i by XREAL_1:232;
((LexBFS:CSeq G) . (G .order())) `2 = ((LexBFS:CSeq G) . i) `2 by A11, Th34;
hence (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i)) by A10, A12; :: thesis: verum

end;

end;