add_ovfl <*FALSE *>,<*FALSE *> <> TRUE by Th14;
then add_ovfl <*FALSE *>,<*FALSE *> = FALSE by XBOOLEAN:def 3;
then <*FALSE *>,<*FALSE *> are_summable by BINARITH:def 10;
then Absval (<*FALSE *> + <*FALSE *>) = (Absval <*FALSE *>) + (Absval <*FALSE *>) by BINARITH:48
.= (Absval <*FALSE *>) + 0 by BINARITH:41
.= Absval <*FALSE *> ;
hence <*FALSE *> + <*FALSE *> = <*FALSE *> by Th2; :: thesis: verum