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₁[ set ] means A c= $1;
A1: star A = { B9 where B9 is Cell of (k + 1),G : S₁[B9] } ;
thus ( B in star A iff S₁[B] ) from LMOD_7:sch 7(A1); :: thesis: verum