let x be Integer; :: thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

per cases ( x < - 2 or ( - 2 <= x & x <= 2 ) or x > 2 ) ;

suppose x < - 2 ; :: thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

hence ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; :: thesis: verum

end;

suppose ( - 2 <= x & x <= 2 ) ; :: thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

hence ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; :: thesis: verum

end;

suppose x > 2 ; :: thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

hence ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; :: thesis: verum

end;

end;