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 B being Cell of (k + 1),G holds

( B in star A iff A c= B )

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

for A being Cell of k,G

for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let G be Grating of d; :: thesis: for A being Cell of k,G

for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let A be Cell of k,G; :: thesis: for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let B be Cell of (k + 1),G; :: thesis: ( B in star A iff A c= B )

defpred S_{1}[ set ] means A c= $1;

A1: star A = { B9 where B9 is Cell of (k + 1),G : S_{1}[B9] }
;

thus ( B in star A iff S_{1}[B] )
from LMOD_7:sch 7(A1); :: thesis: verum

for G being Grating of d

for A being Cell of k,G

for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

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

for A being Cell of k,G

for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let G be Grating of d; :: thesis: for A being Cell of k,G

for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let A be Cell of k,G; :: thesis: for B being Cell of (k + 1),G holds

( B in star A iff A c= B )

let B be Cell of (k + 1),G; :: thesis: ( B in star A iff A c= B )

defpred S

A1: star A = { B9 where B9 is Cell of (k + 1),G : S

thus ( B in star A iff S