thus or2 . <*0 ,0 *> = FALSE 'or' FALSE by Def7
.= 0 ; :: thesis: ( or2 . <*0 ,1*> = 1 & or2 . <*1,0 *> = 1 & or2 . <*1,1*> = 1 & or2a . <*0 ,0 *> = 1 & or2a . <*0 ,1*> = 1 & or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2 . <*0 ,1*> = FALSE 'or' TRUE by Def7
.= 1 ; :: thesis: ( or2 . <*1,0 *> = 1 & or2 . <*1,1*> = 1 & or2a . <*0 ,0 *> = 1 & or2a . <*0 ,1*> = 1 & or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2 . <*1,0 *> = TRUE 'or' FALSE by Def7
.= 1 ; :: thesis: ( or2 . <*1,1*> = 1 & or2a . <*0 ,0 *> = 1 & or2a . <*0 ,1*> = 1 & or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2 . <*1,1*> = TRUE 'or' TRUE by Def7
.= 1 ; :: thesis: ( or2a . <*0 ,0 *> = 1 & or2a . <*0 ,1*> = 1 & or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*0 ,0 *> = TRUE 'or' FALSE by Def8
.= 1 ; :: thesis: ( or2a . <*0 ,1*> = 1 & or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*0 ,1*> = ('not' FALSE ) 'or' TRUE by Def8
.= 1 ; :: thesis: ( or2a . <*1,0 *> = 0 & or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*1,0 *> = ('not' TRUE ) 'or' FALSE by Def8
.= 0 ; :: thesis: ( or2a . <*1,1*> = 1 & or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*1,1*> = ('not' TRUE ) 'or' TRUE by Def8
.= 1 ; :: thesis: ( or2b . <*0 ,0 *> = 1 & or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*0 ,0 *> = TRUE 'or' ('not' FALSE ) by Def9
.= 1 ; :: thesis: ( or2b . <*0 ,1*> = 1 & or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*0 ,1*> = TRUE 'or' ('not' TRUE ) by Def9
.= 1 ; :: thesis: ( or2b . <*1,0 *> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*1,0 *> = ('not' TRUE ) 'or' TRUE by Def9
.= 1 ; :: thesis: or2b . <*1,1*> = 0
thus or2b . <*1,1*> = FALSE 'or' ('not' TRUE ) by Def9
.= 0 ; :: thesis: verum