:: deftheorem Def4 defines Y_equal-in-column GOBOARD1:def 5 :
for M being Matrix of (TOP-REAL 2) holds
( M is Y_equal-in-column iff for n being Nat st n in Seg (width M) holds
Y_axis (Col (M,n)) is constant );