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

( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )

let G be Grating of d; :: thesis: ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )

Omega G = (0_ (d,G)) ` ;

hence ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` ) ; :: thesis: verum

( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )

let G be Grating of d; :: thesis: ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )

Omega G = (0_ (d,G)) ` ;

hence ( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` ) ; :: thesis: verum