cells (d,G) c= cells (d,G) ;
hence cells (d,G) is Chain of d,G ; :: thesis: verum