let i, j be 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: v_strip (G,i) is closed by Th17;
( cell (G,i,j) = (h_strip (G,j)) /\ (v_strip (G,i)) & h_strip (G,j) is closed ) by Th16, GOBOARD5:def 3;
hence cell (G,i,j) is closed by A1, TOPS_1:8; :: thesis: verum