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