let z be Tuple of 1, BOOLEAN ; :: thesis: ( z = <*FALSE*> implies Intval z = 0 )
assume A1: z = <*FALSE*> ; :: thesis: Intval z = 0
len z = 1 by CARD_1:def 7;
then z /. 1 = z . 1 by FINSEQ_4:15
.= FALSE by A1, FINSEQ_1:40 ;
then Intval z = Absval z by BINARI_2:def 3;
hence Intval z = 0 by A1, BINARITH:15; :: thesis: verum