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

for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,G)

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

let G be Grating of d; :: thesis: del (0_ ((k + 1),G)) = 0_ (k,G)

for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,G)

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

let G be Grating of d; :: thesis: del (0_ ((k + 1),G)) = 0_ (k,G)

now :: thesis: for A being Cell of k,G holds

( A in del (0_ ((k + 1),G)) iff A in 0_ (k,G) )

hence
del (0_ ((k + 1),G)) = 0_ (k,G)
by SUBSET_1:3; :: thesis: verum( A in del (0_ ((k + 1),G)) iff A in 0_ (k,G) )

let A be Cell of k,G; :: thesis: ( A in del (0_ ((k + 1),G)) iff A in 0_ (k,G) )

card ((star A) /\ (0_ ((k + 1),G))) = 2 * 0 ;

hence ( A in del (0_ ((k + 1),G)) iff A in 0_ (k,G) ) by Th48; :: thesis: verum

end;card ((star A) /\ (0_ ((k + 1),G))) = 2 * 0 ;

hence ( A in del (0_ ((k + 1),G)) iff A in 0_ (k,G) ) by Th48; :: thesis: verum