add_ovfl (<*FALSE*>,<*TRUE*>) <> TRUE by Th13;
then add_ovfl (<*FALSE*>,<*TRUE*>) = FALSE by XBOOLEAN:def 3;
then <*FALSE*>,<*TRUE*> are_summable by BINARITH:def 7;
then Absval (<*FALSE*> + <*TRUE*>) = (Absval <*FALSE*>) + (Absval <*TRUE*>) by BINARITH:22
.= (Absval <*FALSE*>) + 1 by BINARITH:16
.= 0 + 1 by BINARITH:15
.= Absval <*TRUE*> by BINARITH:16 ;
hence <*FALSE*> + <*TRUE*> = <*TRUE*> by Th2; :: thesis: <*TRUE*> + <*FALSE*> = <*TRUE*>
add_ovfl (<*TRUE*>,<*FALSE*>) <> TRUE by Th13;
then add_ovfl (<*TRUE*>,<*FALSE*>) = FALSE by XBOOLEAN:def 3;
then <*TRUE*>,<*FALSE*> are_summable by BINARITH:def 7;
then Absval (<*TRUE*> + <*FALSE*>) = (Absval <*TRUE*>) + (Absval <*FALSE*>) by BINARITH:22
.= (Absval <*TRUE*>) + 0 by BINARITH:15
.= Absval <*TRUE*> ;
hence <*TRUE*> + <*FALSE*> = <*TRUE*> by Th2; :: thesis: verum