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