let X be set ; for i, k, l, m, n being Nat st X c= Seg i & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l holds
m < n
let i, k, l, m, n be Nat; ( X c= Seg i & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l implies m < n )
assume that
A1:
X c= Seg i
and
A2:
k < l
and
A3:
1 <= n
and
A4:
m <= len (Sgm X)
and
A5:
(Sgm X) . m = k
and
A6:
(Sgm X) . n = l
and
A7:
not m < n
; contradiction
n < m
by A2, A5, A6, A7, XXREAL_0:1;
hence
contradiction
by A1, A2, A3, A4, A5, A6, FINSEQ_1:def 13; verum