thus and3 . <*0 ,0 ,0 *> = (FALSE '&' FALSE ) '&' FALSE by Def16
.= 0 ; :: thesis: ( and3 . <*0 ,0 ,1*> = 0 & and3 . <*0 ,1,0 *> = 0 & and3 . <*0 ,1,1*> = 0 & and3 . <*1,0 ,0 *> = 0 & and3 . <*1,0 ,1*> = 0 & and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*0 ,0 ,1*> = (FALSE '&' FALSE ) '&' TRUE by Def16
.= 0 ; :: thesis: ( and3 . <*0 ,1,0 *> = 0 & and3 . <*0 ,1,1*> = 0 & and3 . <*1,0 ,0 *> = 0 & and3 . <*1,0 ,1*> = 0 & and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*0 ,1,0 *> = (FALSE '&' TRUE ) '&' FALSE by Def16
.= 0 ; :: thesis: ( and3 . <*0 ,1,1*> = 0 & and3 . <*1,0 ,0 *> = 0 & and3 . <*1,0 ,1*> = 0 & and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*0 ,1,1*> = FALSE '&' TRUE by Def16
.= 0 ; :: thesis: ( and3 . <*1,0 ,0 *> = 0 & and3 . <*1,0 ,1*> = 0 & and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,0 ,0 *> = (TRUE '&' FALSE ) '&' FALSE by Def16
.= 0 ; :: thesis: ( and3 . <*1,0 ,1*> = 0 & and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,0 ,1*> = FALSE '&' TRUE by Def16
.= 0 ; :: thesis: ( and3 . <*1,1,0 *> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,1,0 *> = (TRUE '&' TRUE ) '&' FALSE by Def16
.= 0 ; :: thesis: and3 . <*1,1,1*> = 1
thus and3 . <*1,1,1*> = TRUE '&' TRUE by Def16
.= 1 ; :: thesis: verum