let d9 be Nat; :: thesis: for G being Grating of d9 + 1 holds del (Omega G) = 0_ (d9,G)

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

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

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

( A in del (Omega G) iff A in 0_ (d9,G) )

hence
del (Omega G) = 0_ (d9,G)
by SUBSET_1:3; :: thesis: verum( A in del (Omega G) iff A in 0_ (d9,G) )

let A be Cell of d9,G; :: thesis: ( A in del (Omega G) iff A in 0_ (d9,G) )

(star A) /\ (Omega G) = star A by XBOOLE_1:28;

then card ((star A) /\ (Omega G)) = 2 * 1 by Th51;

hence ( A in del (Omega G) iff A in 0_ (d9,G) ) by Th48; :: thesis: verum

end;(star A) /\ (Omega G) = star A by XBOOLE_1:28;

then card ((star A) /\ (Omega G)) = 2 * 1 by Th51;

hence ( A in del (Omega G) iff A in 0_ (d9,G) ) by Th48; :: thesis: verum