consider p being Point of (TOP-REAL 2);
take M = <*<*p*>*>; :: thesis: ( not M is empty-yielding & M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )
A1: len M = 1 by MATRIX_1:25;
A2: width M = 1 by MATRIX_1:25;
hence not M is empty-yielding by A1, Def5; :: thesis: ( M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )
thus M is X_equal-in-line :: thesis: ( M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

proof

let n be Element of NAT ; :: according to GOBOARD1:def 6 :: thesis: ( n in dom M implies X_axis (Line M,n) is constant )
assume n in dom M ; :: thesis: X_axis (Line M,n) is constant
set L = X_axis (Line M,n);
let k be Element of NAT ; :: according to GOBOARD1:def 2 :: thesis: for m being Element of NAT st k in dom (X_axis (Line M,n)) & m in dom (X_axis (Line M,n)) holds
(X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m
let m be Element of NAT ; :: thesis: ( k in dom (X_axis (Line M,n)) & m in dom (X_axis (Line M,n)) implies (X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m )
assume that
A3: k in dom (X_axis (Line M,n)) and
A4: m in dom (X_axis (Line M,n)) ; :: thesis: (X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m
A5: len (X_axis (Line M,n)) = len (Line M,n) by Def3;
k in Seg (len (X_axis (Line M,n))) by A3, FINSEQ_1:def 3;
then k in {1} by A2, A5, FINSEQ_1:4, MATRIX_1:def 8;
then A6: k = 1 by TARSKI:def 1;
m in Seg (len (X_axis (Line M,n))) by A4, FINSEQ_1:def 3;
then m in {1} by A2, A5, FINSEQ_1:4, MATRIX_1:def 8;
hence (X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m by A6, TARSKI:def 1; :: thesis: verum

end;

thus M is Y_equal-in-column :: thesis: ( M is Y_increasing-in-line & M is X_increasing-in-column )

proof

let n be Element of NAT ; :: according to GOBOARD1:def 7 :: thesis: ( n in Seg (width M) implies Y_axis (Col M,n) is constant )
assume n in Seg (width M) ; :: thesis: Y_axis (Col M,n) is constant
set L = Y_axis (Col M,n);
let k be Element of NAT ; :: according to GOBOARD1:def 2 :: thesis: for m being Element of NAT st k in dom (Y_axis (Col M,n)) & m in dom (Y_axis (Col M,n)) holds
(Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m
let m be Element of NAT ; :: thesis: ( k in dom (Y_axis (Col M,n)) & m in dom (Y_axis (Col M,n)) implies (Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m )
assume that
A7: k in dom (Y_axis (Col M,n)) and
A8: m in dom (Y_axis (Col M,n)) ; :: thesis: (Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m
A9: len (Y_axis (Col M,n)) = len (Col M,n) by Def4;
k in Seg (len (Y_axis (Col M,n))) by A7, FINSEQ_1:def 3;
then k in {1} by A1, A9, FINSEQ_1:4, MATRIX_1:def 9;
then A10: k = 1 by TARSKI:def 1;
m in Seg (len (Y_axis (Col M,n))) by A8, FINSEQ_1:def 3;
then m in {1} by A1, A9, FINSEQ_1:4, MATRIX_1:def 9;
hence (Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m by A10, TARSKI:def 1; :: thesis: verum

end;

thus M is Y_increasing-in-line :: thesis: M is X_increasing-in-column

proof

let n be Element of NAT ; :: according to GOBOARD1:def 8 :: thesis: ( n in dom M implies Y_axis (Line M,n) is increasing )
assume n in dom M ; :: thesis: Y_axis (Line M,n) is increasing
set L = Y_axis (Line M,n);
let k be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b₁ being Element of NAT holds
( not k in proj1 (Y_axis (Line M,n)) or not b₁ in proj1 (Y_axis (Line M,n)) or b₁ <= k or not (Y_axis (Line M,n)) . b₁ <= (Y_axis (Line M,n)) . k )
let m be Element of NAT ; :: thesis: ( not k in proj1 (Y_axis (Line M,n)) or not m in proj1 (Y_axis (Line M,n)) or m <= k or not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k )
assume that
A11: k in dom (Y_axis (Line M,n)) and
A12: m in dom (Y_axis (Line M,n)) and
A13: k < m ; :: thesis: not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k
A14: len (Y_axis (Line M,n)) = len (Line M,n) by Def4;
k in Seg (len (Y_axis (Line M,n))) by A11, FINSEQ_1:def 3;
then k in {1} by A2, A14, FINSEQ_1:4, MATRIX_1:def 8;
then A15: k = 1 by TARSKI:def 1;
m in Seg (len (Y_axis (Line M,n))) by A12, FINSEQ_1:def 3;
then m in {1} by A2, A14, FINSEQ_1:4, MATRIX_1:def 8;
hence not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k by A13, A15, TARSKI:def 1; :: thesis: verum

end;

let n be Element of NAT ; :: according to GOBOARD1:def 9 :: thesis: ( n in Seg (width M) implies X_axis (Col M,n) is increasing )
assume n in Seg (width M) ; :: thesis: X_axis (Col M,n) is increasing
set L = X_axis (Col M,n);
let k be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b₁ being Element of NAT holds
( not k in proj1 (X_axis (Col M,n)) or not b₁ in proj1 (X_axis (Col M,n)) or b₁ <= k or not (X_axis (Col M,n)) . b₁ <= (X_axis (Col M,n)) . k )
let m be Element of NAT ; :: thesis: ( not k in proj1 (X_axis (Col M,n)) or not m in proj1 (X_axis (Col M,n)) or m <= k or not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k )
assume that
A16: k in dom (X_axis (Col M,n)) and
A17: m in dom (X_axis (Col M,n)) and
A18: k < m ; :: thesis: not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k
A19: len (X_axis (Col M,n)) = len (Col M,n) by Def3;
k in Seg (len (X_axis (Col M,n))) by A16, FINSEQ_1:def 3;
then k in {1} by A1, A19, FINSEQ_1:4, MATRIX_1:def 9;
then A20: k = 1 by TARSKI:def 1;
m in Seg (len (X_axis (Col M,n))) by A17, FINSEQ_1:def 3;
then m in {1} by A1, A19, FINSEQ_1:4, MATRIX_1:def 9;
hence not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k by A18, A20, TARSKI:def 1; :: thesis: verum