let k be Element of NAT ; :: thesis: for d being non zero Element of 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 Element of 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 set holds not A in del C by A1, Th52;
hence del C = 0_ k,G by XBOOLE_0:def 1; :: thesis: verum