let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for C being Chain of d,G holds C ` = C + (Omega G)
let G be Grating of d; :: thesis: for C being Chain of d,G holds C ` = C + (Omega G)
let C be Chain of d,G; :: thesis: C ` = C + (Omega G)
C /\ (cells d,G) = C by XBOOLE_1:28;
hence C ` = C + (Omega G) by XBOOLE_1:100; :: thesis: verum