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

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