C1 \+\ C2 c= cells (k,G) ;
hence + is Chain of k,G ; :: thesis: verum