for n, m being Element of NAT
for S being set
for Y being Subset of S
for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y