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