thus and3 . <*0,0,0*> = (FALSE '&' FALSE) '&' FALSE by Def9
.= 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 Def9
.= 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 Def9
.= 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 Def9
.= 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 Def9
.= 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 Def9
.= 0 ; :: thesis: ( and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,1,0*> = (TRUE '&' TRUE) '&' FALSE by Def9
.= 0 ; :: thesis: and3 . <*1,1,1*> = 1
thus and3 . <*1,1,1*> = TRUE '&' TRUE by Def9
.= 1 ; :: thesis: verum