let l, m, n, k be Nat; :: thesis: for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n
let X be finite natural-membered set ; :: thesis: ( k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l implies m < n )
assume that
A1: k < l and
A2: m < len (Sgm0 X) and
A3: (Sgm0 X) . m = k and
A4: (Sgm0 X) . n = l and
A5: not m < n ; :: thesis: contradiction
n < m by A1, A3, A4, A5, XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, Def4; :: thesis: verum