let G be _finite _Graph; :: thesis: for m, n being Nat st m < n holds
for x being set st not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x holds
not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x
let m, n be Nat; :: thesis: ( m < n implies for x being set st not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x holds
not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x )
assume m < n ; :: thesis: for x being set st not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x holds
not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x
then m + 1 <= n by NAT_1:13;
then A1: ex j being Nat st (m + 1) + j = n by NAT_1:10;
set CS = LexBFS:CSeq G;
set CSM = (LexBFS:CSeq G) . (m + 1);
set V2M = ((LexBFS:CSeq G) . (m + 1)) `2 ;
let x be set ; :: thesis: ( not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x implies not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x )
assume A2: not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x ; :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x
defpred S<sub>1</sub>[ Nat] means not (G .order()) -' m in (((LexBFS:CSeq G) . ((m + 1) + $1)) `2) . x;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

now :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x

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

suppose A5: (m + 1) + k < G .order() ; :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x

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

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

suppose A7: ( x in G .AdjacentSet {w} & not x in dom (((LexBFS:CSeq G) . ((m + 1) + k)) `1) ) ; :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x

m + 1 <= (m + 1) + k by NAT_1:11;
then m < (m + 1) + k by XREAL_1:39;
then (G .order()) -' m > (G .order()) -' ((m + 1) + k) by A5, Th2;
then A8: not (G .order()) -' m in {((G .order()) -' ((m + 1) + k))} by TARSKI:def 1;
(((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x = ((((LexBFS:CSeq G) . ((m + 1) + k)) `2) . x) \/ {((G .order()) -' ((m + 1) + k))} by A6, A7;
hence not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x by A4, A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( not x in G .AdjacentSet {w} or x in dom (((LexBFS:CSeq G) . ((m + 1) + k)) `1) ) ; :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x

hence not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x by A4, A6; :: thesis: verum

end;

end;

end;

suppose A9: G .order() <= (m + 1) + k ; :: thesis: not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x

(m + 1) + k <= ((m + 1) + k) + 1 by NAT_1:13;
hence not (G .order()) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2) . x by A4, A9, Th34; :: thesis: verum

end;

end;

end;

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

end;

A10: S₁[ 0 ] by A2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A3);
hence not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x by A1; :: thesis: verum