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

now

let A be Cell of d',G; :: thesis: ( A in del (Omega G) iff A in 0_ d',G )
(star A) /\ (Omega G) = star A by XBOOLE_1:28;
then card ((star A) /\ (Omega G)) = 2 * 1 by Th55;
hence ( A in del (Omega G) iff A in 0_ d',G ) by Th52; :: thesis: verum

end;

hence del (Omega G) = 0_ d',G by SUBSET_1:8; :: thesis: verum