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