let d be non zero 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