:: deftheorem defines cell GOBOARD5:def 3 :
for G being Matrix of (TOP-REAL 2)
for i, j being Nat holds cell (G,i,j) = (v_strip (G,i)) /\ (h_strip (G,j));