let k be Element of NAT ; :: thesis: for d being non zero Element of 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 & not card ((star A) /\ C) is even ) )
let d be non zero Element of 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 & not card ((star A) /\ C) is even ) )
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 & not card ((star A) /\ C) is even ) )
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 & not card ((star A) /\ C) is even ) )
let C be Chain of (k + 1),G; :: thesis: ( A in del C iff ( k + 1 <= d & not card ((star A) /\ C) is even ) )
defpred S₁[ Cell of k,G] means ( k + 1 <= d & not card ((star $1) /\ C) is even );
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