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