:: deftheorem Def6 defines X_increasing-in-column GOBOARD1:def 7 :
for M being Matrix of (TOP-REAL 2) holds
( M is X_increasing-in-column iff for n being Nat st n in Seg (width M) holds
X_axis (Col (M,n)) is increasing );