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: 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:35; :: thesis: verum