let k be Nat; :: thesis: for d being non zero Nat

for G being Grating of d

for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let d be non zero Nat; :: thesis: for G being Grating of d

for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let G be Grating of d; :: thesis: for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let A be Cell of k,G; :: thesis: for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let C be Chain of (k + 1),G; :: thesis: ( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

defpred S_{1}[ Cell of k,G] means ( k + 1 <= d & card ((star $1) /\ C) is odd );

A1: del C = { A9 where A9 is Cell of k,G : S_{1}[A9] }
;

thus ( A in del C iff S_{1}[A] )
from LMOD_7:sch 7(A1); :: thesis: verum

for G being Grating of d

for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let d be non zero Nat; :: thesis: for G being Grating of d

for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let G be Grating of d; :: thesis: for A being Cell of k,G

for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let A be Cell of k,G; :: thesis: for C being Chain of (k + 1),G holds

( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

let C be Chain of (k + 1),G; :: thesis: ( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )

defpred S

A1: del C = { A9 where A9 is Cell of k,G : S

thus ( A in del C iff S