let k be Nat; :: thesis: for d being non zero Nat

for G being Grating of d st k + 1 > d holds

for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let d be non zero Nat; :: thesis: for G being Grating of d st k + 1 > d holds

for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let G be Grating of d; :: thesis: ( k + 1 > d implies for C being Chain of (k + 1),G holds del C = 0_ (k,G) )

assume A1: k + 1 > d ; :: thesis: for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let C be Chain of (k + 1),G; :: thesis: del C = 0_ (k,G)

for A being object holds not A in del C by A1, Th48;

hence del C = 0_ (k,G) by XBOOLE_0:def 1; :: thesis: verum

for G being Grating of d st k + 1 > d holds

for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let d be non zero Nat; :: thesis: for G being Grating of d st k + 1 > d holds

for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let G be Grating of d; :: thesis: ( k + 1 > d implies for C being Chain of (k + 1),G holds del C = 0_ (k,G) )

assume A1: k + 1 > d ; :: thesis: for C being Chain of (k + 1),G holds del C = 0_ (k,G)

let C be Chain of (k + 1),G; :: thesis: del C = 0_ (k,G)

for A being object holds not A in del C by A1, Th48;

hence del C = 0_ (k,G) by XBOOLE_0:def 1; :: thesis: verum