set p = the Point of ();
take M = <*<* the Point of ()*>*>; :: thesis: ( M is V3() & 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_0:24;
A2: width M = 1 by MATRIX_0:24;
hence M is V3() by ; :: thesis:
thus M is X_equal-in-line :: thesis:
proof
let n be Nat; :: according to GOBOARD1:def 4 :: 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 Nat; :: according to SEQM_3:def 10 :: thesis: for b1 being set holds
( not k in dom (X_axis (Line (M,n))) or not b1 in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . b1 )

let m be Nat; :: thesis: ( not k in dom (X_axis (Line (M,n))) or not m in dom (X_axis (Line (M,n))) or (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 Def1;
k in Seg (len (X_axis (Line (M,n)))) by ;
then k in {1} by ;
then A6: k = 1 by TARSKI:def 1;
m in Seg (len (X_axis (Line (M,n)))) by ;
then m in {1} by ;
hence (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m by ; :: thesis: verum
end;
thus M is Y_equal-in-column :: thesis:
proof
let n be Nat; :: according to GOBOARD1:def 5 :: thesis: ( n in Seg () implies Y_axis (Col (M,n)) is constant )
assume n in Seg () ; :: thesis: Y_axis (Col (M,n)) is constant
set L = Y_axis (Col (M,n));
let k be Nat; :: according to SEQM_3:def 10 :: thesis: for b1 being set holds
( not k in dom (Y_axis (Col (M,n))) or not b1 in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . b1 )

let m be Nat; :: thesis: ( not k in dom (Y_axis (Col (M,n))) or not m in dom (Y_axis (Col (M,n))) or (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 Def2;
k in Seg (len (Y_axis (Col (M,n)))) by ;
then k in {1} by ;
then A10: k = 1 by TARSKI:def 1;
m in Seg (len (Y_axis (Col (M,n)))) by ;
then m in {1} by ;
hence (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m by ; :: thesis: verum
end;
thus M is Y_increasing-in-line :: thesis:
proof
let n be Nat; :: according to GOBOARD1:def 6 :: 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 Nat; :: according to SEQM_3:def 1 :: thesis: for b1 being set holds
( not k in dom (Y_axis (Line (M,n))) or not b1 in dom (Y_axis (Line (M,n))) or b1 <= k or not (Y_axis (Line (M,n))) . b1 <= (Y_axis (Line (M,n))) . k )

let m be 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 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 Def2;
k in Seg (len (Y_axis (Line (M,n)))) by ;
then k in {1} by ;
then A15: k = 1 by TARSKI:def 1;
m in Seg (len (Y_axis (Line (M,n)))) by ;
then m in {1} by ;
hence not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k by ; :: thesis: verum
end;
let n be Nat; :: according to GOBOARD1:def 7 :: thesis: ( n in Seg () implies X_axis (Col (M,n)) is increasing )
assume n in Seg () ; :: thesis: X_axis (Col (M,n)) is increasing
set L = X_axis (Col (M,n));
let k be Nat; :: according to SEQM_3:def 1 :: thesis: for b1 being set holds
( not k in dom (X_axis (Col (M,n))) or not b1 in dom (X_axis (Col (M,n))) or b1 <= k or not (X_axis (Col (M,n))) . b1 <= (X_axis (Col (M,n))) . k )

let m be 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 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 Def1;
k in Seg (len (X_axis (Col (M,n)))) by ;
then k in {1} by ;
then A20: k = 1 by TARSKI:def 1;
m in Seg (len (X_axis (Col (M,n)))) by ;
then m in {1} by ;
hence not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k by ; :: thesis: verum