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