let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d holds del (0_ (k + 1),G) = 0_ k,G
let d be non zero Element of NAT ; :: thesis: for G being Grating of d holds del (0_ (k + 1),G) = 0_ k,G
let G be Grating of d; :: thesis: del (0_ (k + 1),G) = 0_ k,G

now

let A be Cell of k,G; :: thesis: ( A in del (0_ (k + 1),G) iff A in 0_ k,G )
card ((star A) /\ (0_ (k + 1),G)) = 2 * 0 ;
hence ( A in del (0_ (k + 1),G) iff A in 0_ k,G ) by Th52; :: thesis: verum

end;

hence del (0_ (k + 1),G) = 0_ k,G by SUBSET_1:8; :: thesis: verum