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;