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