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₁[ 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₁[A9] } ;
thus ( A in del C iff S₁[A] ) from LMOD_7:sch 7(A1); :: thesis: verum