let m, k be Nat; :: thesis: for r being Tuple of m + 2,k -SD holds
( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
let r be Tuple of m + 2,k -SD ; :: thesis: ( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
set MZero = SDDec (M0 r);
set R = SDDec r;
assume A1: k >= 2 ; :: thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

now :: thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

per cases ( SDDec r < SDDec (M0 r) or SDDec r >= SDDec (M0 r) ) ;

suppose SDDec r < SDDec (M0 r) ; :: thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

hence ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) by A1, Th4; :: thesis: verum

end;

suppose SDDec r >= SDDec (M0 r) ; :: thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )

hence ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) by A1, Th3; :: thesis: verum

end;

end;

end;

hence ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) ; :: thesis: verum