let k be Nat; :: thesis: for d being non zero Nat
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let d be non zero Nat; :: thesis: for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let G be Grating of d; :: thesis: for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
let C1, C2 be Chain of (k + 1),G; :: thesis: del (C1 + C2) = (del C1) + (del C2)

now :: thesis: for A being Cell of k,G holds
( A in del (C1 + C2) iff A in (del C1) + (del C2) )

let A be Cell of k,G; :: thesis: ( A in del (C1 + C2) iff A in (del C1) + (del C2) )
A1: (star A) /\ (C1 \+\ C2) = ((star A) /\ C1) \+\ ((star A) /\ C2) by XBOOLE_1:112;
A2: ( A in del (C1 + C2) iff ( k + 1 <= d & card ((star A) /\ (C1 \+\ C2)) is odd ) ) by Th48;
A3: ( A in del C1 iff ( k + 1 <= d & card ((star A) /\ C1) is odd ) ) by Th48;
( A in del C2 iff ( k + 1 <= d & card ((star A) /\ C2) is odd ) ) by Th48;
hence ( A in del (C1 + C2) iff A in (del C1) + (del C2) ) by A1, A2, A3, Th7, XBOOLE_0:1; :: thesis: verum

end;

hence del (C1 + C2) = (del C1) + (del C2) by SUBSET_1:3; :: thesis: verum