thus or3 . <*0,0,0*> = FALSE 'or' FALSE by FACIRC_1:def 7
.= 0 ; :: thesis: ( or3 . <*0,0,1*> = 1 & or3 . <*0,1,0*> = 1 & or3 . <*0,1,1*> = 1 & or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*0,0,1*> = (FALSE 'or' FALSE) 'or' TRUE by FACIRC_1:def 7
.= 1 ; :: thesis: ( or3 . <*0,1,0*> = 1 & or3 . <*0,1,1*> = 1 & or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*0,1,0*> = TRUE 'or' FALSE by FACIRC_1:def 7
.= 1 ; :: thesis: ( or3 . <*0,1,1*> = 1 & or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*0,1,1*> = (FALSE 'or' TRUE) 'or' TRUE by FACIRC_1:def 7
.= 1 ; :: thesis: ( or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,0,0*> = TRUE 'or' FALSE by FACIRC_1:def 7
.= 1 ; :: thesis: ( or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,0,1*> = (TRUE 'or' FALSE) 'or' TRUE by FACIRC_1:def 7
.= 1 ; :: thesis: ( or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,1,0*> = (TRUE 'or' TRUE) 'or' FALSE by FACIRC_1:def 7
.= 1 ; :: thesis: or3 . <*1,1,1*> = 1
thus or3 . <*1,1,1*> = (TRUE 'or' TRUE) 'or' TRUE by FACIRC_1:def 7
.= 1 ; :: thesis: verum