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 & width M = 1 & Indices M = [:(Seg 1),(Seg 1):] ) by MATRIX_1:25;
hence not M is empty-yielding by 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 ( k in dom (X_axis (Line M,n)) & m in dom (X_axis (Line M,n)) ) ; :: thesis: (X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m
then ( k in Seg (len (X_axis (Line M,n))) & m in Seg (len (X_axis (Line M,n))) & len (X_axis (Line M,n)) = len (Line M,n) ) by Def3, FINSEQ_1:def 3;
then ( k in {1} & m in {1} ) by A1, FINSEQ_1:4, MATRIX_1:def 8;
then ( k = 1 & m = 1 ) by TARSKI:def 1;
hence (X_axis (Line M,n)) . k = (X_axis (Line M,n)) . m ; :: 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 ( k in dom (Y_axis (Col M,n)) & m in dom (Y_axis (Col M,n)) ) ; :: thesis: (Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m
then ( k in Seg (len (Y_axis (Col M,n))) & m in Seg (len (Y_axis (Col M,n))) & len (Y_axis (Col M,n)) = len (Col M,n) ) by Def4, FINSEQ_1:def 3;
then ( k in {1} & m in {1} ) by A1, FINSEQ_1:4, MATRIX_1:def 9;
then ( k = 1 & m = 1 ) by TARSKI:def 1;
hence (Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . m ; :: 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 dom (Y_axis (Line M,n)) or not b₁ in dom (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 dom (Y_axis (Line M,n)) or not m in dom (Y_axis (Line M,n)) or m <= k or not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k )
assume A2: ( k in dom (Y_axis (Line M,n)) & m in dom (Y_axis (Line M,n)) & k < m ) ; :: thesis: not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k
then ( k in Seg (len (Y_axis (Line M,n))) & m in Seg (len (Y_axis (Line M,n))) & len (Y_axis (Line M,n)) = len (Line M,n) ) by Def4, FINSEQ_1:def 3;
then ( k in {1} & m in {1} ) by A1, FINSEQ_1:4, MATRIX_1:def 8;
then ( k = 1 & m = 1 ) by TARSKI:def 1;
hence not (Y_axis (Line M,n)) . m <= (Y_axis (Line M,n)) . k by A2; :: 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 dom (X_axis (Col M,n)) or not b₁ in dom (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 dom (X_axis (Col M,n)) or not m in dom (X_axis (Col M,n)) or m <= k or not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k )
assume A3: ( k in dom (X_axis (Col M,n)) & m in dom (X_axis (Col M,n)) & k < m ) ; :: thesis: not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k
then ( k in Seg (len (X_axis (Col M,n))) & m in Seg (len (X_axis (Col M,n))) & len (X_axis (Col M,n)) = len (Col M,n) ) by Def3, FINSEQ_1:def 3;
then ( k in {1} & m in {1} ) by A1, FINSEQ_1:4, MATRIX_1:def 9;
then ( k = 1 & m = 1 ) by TARSKI:def 1;
hence not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k by A3; :: thesis: verum