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 FINSEQ_1:def 18;
then z /. 1 = z . 1 by FINSEQ_4:24
.= FALSE by A1, FINSEQ_1:57 ;
then Intval z = Absval z by BINARI_2:def 3;
hence Intval z = 0 by A1, BINARITH:41; :: thesis: verum