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 CARD_1:def 7;
then z /. 1 = z . 1 by FINSEQ_4:15
.= TRUE by A1, FINSEQ_1:40 ;
then Intval z = (Absval z) - (2 to_power 1) by BINARI_2:def 3
.= 1 - (2 to_power 1) by A1, BINARITH:16
.= 1 - (1 + 1) by POWER:25
.= 0 - 1 ;
hence Intval z = - 1 ; :: thesis: verum