let m, k be Nat; :: thesis: for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)
let r be Tuple of m + 2,k -SD ; :: thesis: ( m >= 1 & k >= 2 & SDDec (Mmask r) > 0 implies SDDec r > SDDec (M0 r) )
assume that
A1: m >= 1 and
A2: k >= 2 ; :: thesis: ( not SDDec (Mmask r) > 0 or SDDec r > SDDec (M0 r) )
A3: m + 2 > 1 by A1, Lm1;
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k))) by A2, Th17
.= (SDDec r) + 0 by A3, RADIX_5:6 ;
then A4: (SDDec r) - (SDDec (M0 r)) = (SDDec (Mmask r)) - 0 ;
assume SDDec (Mmask r) > 0 ; :: thesis: SDDec r > SDDec (M0 r)
hence SDDec r > SDDec (M0 r) by A4, XREAL_1:47; :: thesis: verum