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

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