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: S₁[ 0 ]

proof

(LexBFS:CSeq G) . 0 = LexBFS:Init G by Def33;
then (((LexBFS:CSeq G) . 0 ) `2 ) . v = {} by Th38;
hence S₁[ 0 ] by XBOOLE_1:2; :: thesis: verum

end;

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 CSK = (LexBFS:CSeq G) . k;
set V2K = ((LexBFS:CSeq G) . k) `2 ;
set VLK = ((LexBFS:CSeq G) . k) `1 ;
set CK1 = (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 A4: k < G .order() by NAT_1:13;
then consider w being Vertex of G such that
w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . k) and
A5: 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 Th54;

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 ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . k) `1 ) ) ; :: thesis: S₁[k + 1]

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

end;

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

then A7: (((LexBFS:CSeq G) . (k + 1)) `2 ) . v = (((LexBFS:CSeq G) . k) `2 ) . v by A5;
k <= k + 1 by NAT_1:13;
then (Seg (G .order() )) \ (Seg ((G .order() ) -' k)) c= (Seg (G .order() )) \ (Seg ((G .order() ) -' (k + 1))) by Th6;
hence S₁[k + 1] by A3, A7, 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;

A8: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);

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 A8; :: thesis: verum

end;

suppose A9: 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:11;
then (G .order() ) -' i = 0 by XREAL_0:def 2;
then A10: (G .order() ) -' (G .order() ) = (G .order() ) -' i by XREAL_1:234;
((LexBFS:CSeq G) . (G .order() )) `2 = ((LexBFS:CSeq G) . i) `2 by A9, Th48;
hence (((LexBFS:CSeq G) . i) `2 ) . v c= (Seg (G .order() )) \ (Seg ((G .order() ) -' i)) by A8, A10; :: thesis: verum

end;

end;