let X be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: contradiction
n < m by A2, A5, A6, A7, XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, A5, A6, FINSEQ_1:def 13; :: thesis: verum