thus and2 . <*0 ,0 *> = FALSE '&' FALSE by Def1
.= 0 ; :: thesis: ( and2 . <*0 ,1*> = 0 & and2 . <*1,0 *> = 0 & and2 . <*1,1*> = 1 & and2a . <*0 ,0 *> = 0 & and2a . <*0 ,1*> = 1 & and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*0 ,1*> = FALSE '&' TRUE by Def1
.= 0 ; :: thesis: ( and2 . <*1,0 *> = 0 & and2 . <*1,1*> = 1 & and2a . <*0 ,0 *> = 0 & and2a . <*0 ,1*> = 1 & and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*1,0 *> = TRUE '&' FALSE by Def1
.= 0 ; :: thesis: ( and2 . <*1,1*> = 1 & and2a . <*0 ,0 *> = 0 & and2a . <*0 ,1*> = 1 & and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*1,1*> = TRUE '&' TRUE by Def1
.= 1 ; :: thesis: ( and2a . <*0 ,0 *> = 0 & and2a . <*0 ,1*> = 1 & and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*0 ,0 *> = ('not' FALSE ) '&' FALSE by Def2
.= 0 ; :: thesis: ( and2a . <*0 ,1*> = 1 & and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*0 ,1*> = ('not' FALSE ) '&' TRUE by Def2
.= 1 ; :: thesis: ( and2a . <*1,0 *> = 0 & and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,0 *> = ('not' TRUE ) '&' FALSE by Def2
.= 0 ; :: thesis: ( and2a . <*1,1*> = 0 & and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,1*> = ('not' TRUE ) '&' TRUE by Def2
.= 0 ; :: thesis: ( and2b . <*0 ,0 *> = 1 & and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0 ,0 *> = TRUE '&' ('not' FALSE ) by Def3
.= 1 ; :: thesis: ( and2b . <*0 ,1*> = 0 & and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0 ,1*> = ('not' FALSE ) '&' ('not' TRUE ) by Def3
.= 0 ; :: thesis: ( and2b . <*1,0 *> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*1,0 *> = ('not' TRUE ) '&' ('not' FALSE ) by Def3
.= 0 ; :: thesis: and2b . <*1,1*> = 0
thus and2b . <*1,1*> = FALSE '&' ('not' TRUE ) by Def3
.= 0 ; :: thesis: verum