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 A1: 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
set CS = LexBFS:CSeq G;
set CSM = (LexBFS:CSeq G) . (m + 1);
set V2M = ((LexBFS:CSeq G) . (m + 1)) `2 ;
set CSN = (LexBFS:CSeq G) . n;
set V2N = ((LexBFS:CSeq G) . n) `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₁[ Nat] means not (G .order() ) -' m in (((LexBFS:CSeq G) . ((m + 1) + $1)) `2 ) . x;
A3: S₁[ 0 ] by A2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: 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

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

suppose A6: (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
A7: 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 Th54;

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 ( 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

then A8: (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2 ) . x = ((((LexBFS:CSeq G) . ((m + 1) + k)) `2 ) . x) \/ {((G .order() ) -' ((m + 1) + k))} by A7;
( m < m + 1 & m + 1 <= (m + 1) + k ) by NAT_1:11, XREAL_1:41;
then m < (m + 1) + k by XXREAL_0:2;
then (G .order() ) -' m > (G .order() ) -' ((m + 1) + k) by A6, Th2;
then not (G .order() ) -' m in {((G .order() ) -' ((m + 1) + k))} by TARSKI:def 1;
hence not (G .order() ) -' m in (((LexBFS:CSeq G) . (((m + 1) + k) + 1)) `2 ) . x by A5, 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 A5, A7; :: 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 A5, A9, Th48; :: thesis: verum

end;

end;

end;

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

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
m + 1 <= n by A1, NAT_1:13;
then ex j being Nat st (m + 1) + j = n by NAT_1:10;
hence not (G .order() ) -' m in (((LexBFS:CSeq G) . n) `2 ) . x by A10; :: thesis: verum