let G be _finite _Graph; :: thesis: for m, n, k being Nat st k < n & n <= m holds
for x being set st not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x holds
not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x
let m, n, k be Nat; :: thesis: ( k < n & n <= m implies for x being set st not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x holds
not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x )
assume that
A1: k < n and
A2: n <= m ; :: thesis: for x being set st not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x holds
not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x
set CS = LexBFS:CSeq G;
set CSN = (LexBFS:CSeq G) . n;
set V2N = ((LexBFS:CSeq G) . n) `2 ;
let x be set ; :: thesis: ( not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x implies not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x )
assume A3: not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x ; :: thesis: not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x
set CK1 = (LexBFS:CSeq G) . (k + 1);
set V21 = ((LexBFS:CSeq G) . (k + 1)) `2 ;
k + 1 <= n by A1, NAT_1:13;
then (((LexBFS:CSeq G) . (k + 1)) `2) . x c= (((LexBFS:CSeq G) . n) `2) . x by Th44;
then A4: not (G .order()) -' k in (((LexBFS:CSeq G) . (k + 1)) `2) . x by A3;
k < m by A1, A2, XXREAL_0:2;
hence not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x by A4, Th46; :: thesis: verum