:: deftheorem Def3 defines X_equal-in-line GOBOARD1:def 4 :
for M being Matrix of (TOP-REAL 2) holds
( M is X_equal-in-line iff for n being Nat st n in dom M holds
X_axis (Line (M,n)) is constant );