let m, k be Nat; :: thesis: for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & not ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) holds
( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) )
let r be Tuple of (m + 2),(k -SD ); :: thesis: ( m >= 1 & k >= 2 & not ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) implies ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
assume A1: ( m >= 1 & k >= 2 ) ; :: thesis: ( ( 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;

now

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