let i, j be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) holds cell G,i,j is closed
let G be Matrix of (TOP-REAL 2); :: thesis: cell G,i,j is closed
A1: cell G,i,j = (h_strip G,j) /\ (v_strip G,i) by GOBOARD5:def 3;
A2: h_strip G,j is closed by Th16;
v_strip G,i is closed by Th17;
hence cell G,i,j is closed by A1, A2, TOPS_1:35; :: thesis: verum