let z be Tuple of 1, BOOLEAN ; :: thesis: ( z = <*TRUE *> implies Intval z = - 1 )
assume A1: z = <*TRUE *> ; :: thesis: Intval z = - 1
len z = 1 by FINSEQ_1:def 18;
then z /. 1 = z . 1 by FINSEQ_4:24
.= TRUE by A1, FINSEQ_1:57 ;
then Intval z = (Absval z) - (2 to_power 1) by BINARI_2:def 3
.= 1 - (2 to_power 1) by A1, BINARITH:42
.= 1 - (1 + 1) by POWER:30
.= 0 - 1 ;
hence Intval z = - 1 ; :: thesis: verum