A1:
add_ovfl (<*TRUE*>,<*TRUE*>) = TRUE
by Th13;
Absval (<*TRUE*> + <*TRUE*>) =
((Absval (<*TRUE*> + <*TRUE*>)) + 2) - 2
.=
((Absval (<*TRUE*> + <*TRUE*>)) + (2 to_power 1)) - 2
by POWER:25
.=
((Absval (<*TRUE*> + <*TRUE*>)) + (IFEQ ((add_ovfl (<*TRUE*>,<*TRUE*>)),FALSE,0,(2 to_power 1)))) - 2
by A1, FUNCOP_1:def 8
.=
((Absval <*TRUE*>) + (Absval <*TRUE*>)) - 2
by BINARITH:21
.=
((Absval <*TRUE*>) + 1) - 2
by BINARITH:16
.=
(1 + 1) - 2
by BINARITH:16
.=
Absval <*FALSE*>
by BINARITH:15
;
hence
<*TRUE*> + <*TRUE*> = <*FALSE*>
by Th2; verum