:: BINARITH semantic presentation

definition
let c1 be Nat;
let c2 be non empty set ;
mode Tuple is Element of a1 -tuples_on a2;
end;

Lemma1: for b1, b2 being Nat holds addnat . b1,b2 = b1 + b2
by BINOP_2:def 23;

theorem Th1: :: BINARITH:1
canceled;

theorem Th2: :: BINARITH:2
for b1, b2 being Nat
for b3 being non empty set
for b4 being Element of b3
for b5 being Tuple of b2,b3 holds
( b1 in Seg b2 implies (b5 ^ <*b4*>) /. b1 = b5 /. b1 )
proof
let c1, c2 be Nat;
let c3 be non empty set ;
let c4 be Element of c3;
let c5 be Tuple of c2,c3;
assume E3: c1 in Seg c2 ;
len c5 = c2 by FINSEQ_2:109;
then c1 in dom c5 by E3, FINSEQ_1:def 3;
hence (c5 ^ <*c4*>) /. c1 = c5 /. c1 by FINSEQ_4:83;
end;

theorem Th3: :: BINARITH:3
for b1 being Nat
for b2 being non empty set
for b3 being Element of b2
for b4 being Tuple of b1,b2 holds (b4 ^ <*b3*>) /. (b1 + 1) = b3
proof
let c1 be Nat;
let c2 be non empty set ;
let c3 be Element of c2;
let c4 be Tuple of c1,c2;
len <*c3*> = 1 by FINSEQ_1:56;
then 0 + 1 in Seg (len <*c3*>) ;
then E4: 0 + 1 in dom <*c3*> by FINSEQ_1:def 3;
len c4 = c1 by FINSEQ_2:109;
hence (c4 ^ <*c3*>) /. (c1 + 1) = <*c3*> /. 1 by E4, FINSEQ_4:84
.= c3 by FINSEQ_4:25 ;

end;

theorem Th4: :: BINARITH:4
canceled;

theorem Th5: :: BINARITH:5
for b1, b2 being Nat holds
not ( b1 in Seg b2 & b1 is empty ) by CARD_1:51, FINSEQ_1:3;

definition
let c1, c2 be boolean set ;
func c1 'or' c2 -> set equals :: BINARITH:def 1
 'not' (('not' a1) '&' ('not' a2));
correctness
coherence
'not' (('not' c1) '&' ('not' c2)) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = 'not' (('not' b2) '&' ('not' b3)) implies b1 = 'not' (('not' b3) '&' ('not' b2)) ) ;
end;

:: deftheorem Def1 defines 'or' BINARITH:def 1 :
for b1, b2 being boolean set holds b1 'or' b2 = 'not' (('not' b1) '&' ('not' b2));

definition
let c1, c2 be boolean set ;
func c1 'xor' c2 -> set equals :: BINARITH:def 2
(('not' a1) '&' a2) 'or' (a1 '&' ('not' a2));
correctness
coherence
(('not' c1) '&' c2) 'or' (c1 '&' ('not' c2)) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = (('not' b2) '&' b3) 'or' (b2 '&' ('not' b3)) implies b1 = (('not' b3) '&' b2) 'or' (b3 '&' ('not' b2)) ) ;
end;

:: deftheorem Def2 defines 'xor' BINARITH:def 2 :
for b1, b2 being boolean set holds b1 'xor' b2 = (('not' b1) '&' b2) 'or' (b1 '&' ('not' b2));

registration
let c1, c2 be boolean set ;
cluster a1 'or' a2 -> boolean ;
correctness
coherence
c1 'or' c2 is boolean;
;
end;

registration
let c1, c2 be boolean set ;
cluster a1 'xor' a2 -> boolean ;
correctness
coherence
c1 'xor' c2 is boolean;
;
end;

definition
let c1, c2 be Element of BOOLEAN ;
redefine func 'or' as c1 'or' c2 -> Element of BOOLEAN ;
correctness
coherence
c1 'or' c2 is Element of BOOLEAN ;
by MARGREL1:def 15;
redefine func 'xor' as c1 'xor' c2 -> Element of BOOLEAN ;
correctness
coherence
c1 'xor' c2 is Element of BOOLEAN ;
by MARGREL1:def 15;
end;

theorem Th6: :: BINARITH:6
canceled;

theorem Th7: :: BINARITH:7
for b1 being boolean set holds b1 'or' FALSE = b1
proof
let c1 be boolean set ;
thus c1 'or' FALSE = 'not' (('not' c1) '&' ('not' FALSE ))
.= 'not' (TRUE '&' ('not' c1)) by MARGREL1:41
.= 'not' ('not' c1) by MARGREL1:50
.= c1 ;
end;

theorem Th8: :: BINARITH:8
canceled;

theorem Th9: :: BINARITH:9
for b1, b2 being boolean set holds 'not' (b1 '&' b2) = ('not' b1) 'or' ('not' b2) ;

theorem Th10: :: BINARITH:10
for b1, b2 being boolean set holds 'not' (b1 'or' b2) = ('not' b1) '&' ('not' b2) ;

theorem Th11: :: BINARITH:11
canceled;

theorem Th12: :: BINARITH:12
for b1, b2 being boolean set holds b1 '&' b2 = 'not' (('not' b1) 'or' ('not' b2)) ;

theorem Th13: :: BINARITH:13
for b1 being boolean set holds TRUE 'xor' b1 = 'not' b1
proof
let c1 be boolean set ;
thus TRUE 'xor' c1 = (('not' TRUE ) '&' c1) 'or' (TRUE '&' ('not' c1))
.= (FALSE '&' c1) 'or' (TRUE '&' ('not' c1)) by MARGREL1:def 16
.= FALSE 'or' (TRUE '&' ('not' c1)) by MARGREL1:49
.= FALSE 'or' ('not' c1) by MARGREL1:50
.= 'not' c1 by Th7 ;
end;

theorem Th14: :: BINARITH:14
for b1 being boolean set holds FALSE 'xor' b1 = b1
proof
let c1 be boolean set ;
thus FALSE 'xor' c1 = (('not' FALSE ) '&' c1) 'or' (FALSE '&' ('not' c1))
.= (TRUE '&' c1) 'or' (FALSE '&' ('not' c1)) by MARGREL1:def 16
.= c1 'or' (FALSE '&' ('not' c1)) by MARGREL1:50
.= c1 'or' FALSE by MARGREL1:49
.= c1 by Th7 ;
end;

theorem Th15: :: BINARITH:15
for b1 being boolean set holds b1 'xor' b1 = FALSE
proof
let c1 be boolean set ;
thus c1 'xor' c1 = (('not' c1) '&' c1) 'or' (c1 '&' ('not' c1))
.= (c1 '&' ('not' c1)) 'or' FALSE by MARGREL1:46
.= FALSE 'or' FALSE by MARGREL1:46
.= FALSE by Th7 ;
end;

theorem Th16: :: BINARITH:16
for b1 being boolean set holds b1 '&' b1 = b1
proof
let c1 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 '&' c1 = c1 by MARGREL1:45;
end;
suppose c1 = FALSE ;
hence c1 '&' c1 = c1 by MARGREL1:45;
end;
end;
end;

theorem Th17: :: BINARITH:17
for b1 being boolean set holds b1 'xor' ('not' b1) = TRUE
proof
let c1 be boolean set ;
thus c1 'xor' ('not' c1) = (('not' c1) '&' ('not' c1)) 'or' (c1 '&' ('not' ('not' c1)))
.= (('not' c1) '&' ('not' c1)) 'or' (c1 '&' c1)
.= ('not' c1) 'or' (c1 '&' c1) by Th16
.= ('not' c1) 'or' c1 by Th16
.= 'not' (('not' ('not' c1)) '&' ('not' c1))
.= TRUE by MARGREL1:47 ;
end;

theorem Th18: :: BINARITH:18
for b1 being boolean set holds b1 'or' ('not' b1) = TRUE by MARGREL1:47;

theorem Th19: :: BINARITH:19
for b1 being boolean set holds b1 'or' TRUE = TRUE
proof
let c1 be boolean set ;
thus c1 'or' TRUE = 'not' (('not' c1) '&' ('not' TRUE ))
.= 'not' (FALSE '&' ('not' c1)) by MARGREL1:def 16
.= 'not' FALSE by MARGREL1:49
.= TRUE by MARGREL1:def 16 ;
end;

theorem Th20: :: BINARITH:20
for b1, b2, b3 being boolean set holds (b1 'or' b2) 'or' b3 = b1 'or' (b2 'or' b3) by MARGREL1:52;

theorem Th21: :: BINARITH:21
for b1 being boolean set holds b1 'or' b1 = b1
proof
let c1 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 'or' c1 = c1 by Th19;
end;
suppose c1 = FALSE ;
hence c1 'or' c1 = c1 by Th7;
end;
end;
end;

theorem Th22: :: BINARITH:22
for b1, b2, b3 being boolean set holds b1 '&' (b2 'or' b3) = (b1 '&' b2) 'or' (b1 '&' b3)
proof
let c1, c2, c3 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E13: c1 = TRUE ;
hence c1 '&' (c2 'or' c3) = c2 'or' c3 by MARGREL1:50
.= (c1 '&' c2) 'or' c3 by E13, MARGREL1:50
.= (c1 '&' c2) 'or' (c1 '&' c3) by E13, MARGREL1:50 ;

end;
suppose E13: c1 = FALSE ;
hence c1 '&' (c2 'or' c3) = c1 by MARGREL1:49
.= c1 'or' c1 by E13, Th7
.= (c1 '&' c2) 'or' c1 by E13, MARGREL1:49
.= (c1 '&' c2) 'or' (c1 '&' c3) by E13, MARGREL1:49 ;

end;
end;
end;

theorem Th23: :: BINARITH:23
for b1, b2, b3 being boolean set holds b1 'or' (b2 '&' b3) = (b1 'or' b2) '&' (b1 'or' b3)
proof
let c1, c2, c3 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E14: c1 = TRUE ;
hence c1 'or' (c2 '&' c3) = c1 by Th19
.= c1 '&' c1 by Th16
.= (c1 'or' c2) '&' c1 by E14, Th19
.= (c1 'or' c2) '&' (c1 'or' c3) by E14, Th19 ;

end;
suppose E14: c1 = FALSE ;
hence c1 'or' (c2 '&' c3) = c2 '&' c3 by Th7
.= (c1 'or' c2) '&' c3 by E14, Th7
.= (c1 'or' c2) '&' (c1 'or' c3) by E14, Th7 ;

end;
end;
end;

theorem Th24: :: BINARITH:24
for b1, b2 being boolean set holds b1 'or' (b1 '&' b2) = b1
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 'or' (c1 '&' c2) = c1 by Th19;
end;
suppose E14: c1 = FALSE ;
then c1 'or' (c1 '&' c2) = c1 '&' c2 by Th7
.= c1 by E14, MARGREL1:49 ;
hence c1 'or' (c1 '&' c2) = c1 ;
end;
end;
end;

theorem Th25: :: BINARITH:25
for b1, b2 being boolean set holds b1 '&' (b1 'or' b2) = b1
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E15: c1 = TRUE ;
then c1 '&' (c1 'or' c2) = c1 '&' c1 by Th19
.= c1 by E15, MARGREL1:50 ;
hence c1 '&' (c1 'or' c2) = c1 ;
end;
suppose c1 = FALSE ;
hence c1 '&' (c1 'or' c2) = c1 by MARGREL1:49;
end;
end;
end;

theorem Th26: :: BINARITH:26
for b1, b2 being boolean set holds b1 'or' (('not' b1) '&' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E16: c1 = TRUE ;
then c1 'or' (('not' c1) '&' c2) = c1 'or' (FALSE '&' c2) by MARGREL1:def 16
.= c1 'or' FALSE by MARGREL1:49
.= c1 by Th7
.= c1 'or' c2 by E16, Th19 ;
hence c1 'or' (('not' c1) '&' c2) = c1 'or' c2 ;
end;
suppose c1 = FALSE ;
then c1 'or' (('not' c1) '&' c2) = c1 'or' (TRUE '&' c2) by MARGREL1:def 16
.= c1 'or' c2 by MARGREL1:50 ;
hence c1 'or' (('not' c1) '&' c2) = c1 'or' c2 ;
end;
end;
end;

theorem Th27: :: BINARITH:27
for b1, b2 being boolean set holds b1 '&' (('not' b1) 'or' b2) = b1 '&' b2
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
then c1 '&' (('not' c1) 'or' c2) = c1 '&' (FALSE 'or' c2) by MARGREL1:def 16
.= c1 '&' c2 by Th7 ;
hence c1 '&' (('not' c1) 'or' c2) = c1 '&' c2 ;
end;
suppose E16: c1 = FALSE ;
then c1 '&' (('not' c1) 'or' c2) = c1 by MARGREL1:49
.= c1 '&' c2 by E16, MARGREL1:49 ;
hence c1 '&' (('not' c1) 'or' c2) = c1 '&' c2 ;
end;
end;
end;

theorem Th28: :: BINARITH:28
canceled;

theorem Th29: :: BINARITH:29
canceled;

theorem Th30: :: BINARITH:30
canceled;

theorem Th31: :: BINARITH:31
canceled;

theorem Th32: :: BINARITH:32
canceled;

theorem Th33: :: BINARITH:33
TRUE 'xor' FALSE = TRUE
proof
thus TRUE 'xor' FALSE = TRUE 'xor' ('not' TRUE ) by MARGREL1:41
.= TRUE by Th17 ;
end;

theorem Th34: :: BINARITH:34
for b1, b2, b3 being boolean set holds (b1 'xor' b2) 'xor' b3 = b1 'xor' (b2 'xor' b3)
proof
let c1, c2, c3 be boolean set ;
E18: (('not' (('not' c1) '&' c2)) '&' ('not' (c1 '&' ('not' c2)))) '&' c3 = (c1 'or' ('not' c2)) '&' (c3 '&' (('not' c1) 'or' c2)) by MARGREL1:52
.= (c1 'or' ('not' c2)) '&' ((c3 '&' ('not' c1)) 'or' (c3 '&' c2)) by Th22
.= ((c1 'or' ('not' c2)) '&' (c3 '&' ('not' c1))) 'or' ((c1 'or' ('not' c2)) '&' (c3 '&' c2)) by Th22 ;
E19: (c1 'or' ('not' c2)) '&' (c3 '&' ('not' c1)) = ((c3 '&' ('not' c1)) '&' c1) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by Th22
.= (c3 '&' (('not' c1) '&' c1)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= (c3 '&' FALSE ) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:46
.= FALSE 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:49
.= (c3 '&' ('not' c1)) '&' ('not' c2) by Th7 ;
E20: (c1 'or' ('not' c2)) '&' (c3 '&' c2) = ((c3 '&' c2) '&' c1) 'or' ((c3 '&' c2) '&' ('not' c2)) by Th22
.= ((c3 '&' c2) '&' c1) 'or' (c3 '&' (c2 '&' ('not' c2))) by MARGREL1:52
.= ((c3 '&' c2) '&' c1) 'or' (c3 '&' FALSE ) by MARGREL1:46
.= ((c3 '&' c2) '&' c1) 'or' FALSE by MARGREL1:49
.= (c3 '&' c2) '&' c1 by Th7 ;
((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) '&' ('not' c3) = (('not' c3) '&' (('not' c1) '&' c2)) 'or' (('not' c3) '&' (c1 '&' ('not' c2))) by Th22
.= ((('not' c3) '&' ('not' c1)) '&' c2) 'or' (('not' c3) '&' (c1 '&' ('not' c2))) by MARGREL1:52
.= ((('not' c3) '&' ('not' c1)) '&' c2) 'or' ((('not' c3) '&' c1) '&' ('not' c2)) by MARGREL1:52 ;
then E21: (c1 'xor' c2) 'xor' c3 = (((c3 '&' c2) '&' c1) 'or' (((('not' c3) '&' ('not' c1)) '&' c2) 'or' ((('not' c3) '&' c1) '&' ('not' c2)))) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by E18, E19, E20, Th20
.= ((((c3 '&' c2) '&' c1) 'or' ((('not' c3) '&' c1) '&' ('not' c2))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by Th20
.= ((((c1 '&' c2) '&' c3) 'or' ((('not' c3) '&' c1) '&' ('not' c2))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by MARGREL1:52 ;
E22: c1 'xor' (c2 'xor' c3) = c1 'xor' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' (c1 '&' ('not' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))))
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' (c1 '&' (('not' (('not' c2) '&' c3)) '&' ('not' (c2 '&' ('not' c3)))))
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' ((c1 '&' ('not' (('not' c2) '&' c3))) '&' ('not' (c2 '&' ('not' c3)))) by MARGREL1:52 ;
E23: ('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) = (('not' c1) '&' (('not' c2) '&' c3)) 'or' (('not' c1) '&' (c2 '&' ('not' c3))) by Th22
.= ((('not' c1) '&' ('not' c2)) '&' c3) 'or' (('not' c1) '&' (c2 '&' ('not' c3))) by MARGREL1:52
.= ((('not' c1) '&' ('not' c2)) '&' c3) 'or' ((('not' c1) '&' c2) '&' ('not' c3)) by MARGREL1:52 ;
E24: 'not' (('not' c2) '&' c3) = ('not' ('not' c2)) 'or' ('not' c3)
.= c2 'or' ('not' c3) ;
E25: (c1 '&' ('not' (('not' c2) '&' c3))) '&' ('not' (c2 '&' ('not' c3))) = (('not' c2) 'or' c3) '&' ((c1 '&' c2) 'or' (c1 '&' ('not' c3))) by E24, Th22
.= ((('not' c2) 'or' c3) '&' (c1 '&' c2)) 'or' ((('not' c2) 'or' c3) '&' (c1 '&' ('not' c3))) by Th22 ;
E26: (('not' c2) 'or' c3) '&' (c1 '&' c2) = ((c1 '&' c2) '&' ('not' c2)) 'or' ((c1 '&' c2) '&' c3) by Th22
.= (c1 '&' (c2 '&' ('not' c2))) 'or' ((c1 '&' c2) '&' c3) by MARGREL1:52
.= (c1 '&' FALSE ) 'or' ((c1 '&' c2) '&' c3) by MARGREL1:46
.= FALSE 'or' ((c1 '&' c2) '&' c3) by MARGREL1:49
.= (c1 '&' c2) '&' c3 by Th7 ;
(('not' c2) 'or' c3) '&' (c1 '&' ('not' c3)) = ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' ((c1 '&' ('not' c3)) '&' c3) by Th22
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' (c1 '&' (('not' c3) '&' c3)) by MARGREL1:52
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' (c1 '&' FALSE ) by MARGREL1:46
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' FALSE by MARGREL1:49
.= (c1 '&' ('not' c3)) '&' ('not' c2) by Th7 ;
then c1 'xor' (c2 'xor' c3) = ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c3)) '&' ('not' c2))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by E22, E23, E25, E26, Th20
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by MARGREL1:52 ;
hence (c1 'xor' c2) 'xor' c3 = c1 'xor' (c2 'xor' c3) by E21;
end;

theorem Th35: :: BINARITH:35
for b1, b2 being boolean set holds b1 'xor' (('not' b1) '&' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
thus c1 'xor' (('not' c1) '&' c2) = (('not' c1) '&' (('not' c1) '&' c2)) 'or' (c1 '&' ('not' (('not' c1) '&' c2)))
.= ((('not' c1) '&' ('not' c1)) '&' c2) 'or' (c1 '&' ('not' (('not' c1) '&' c2))) by MARGREL1:52
.= (('not' c1) '&' c2) 'or' (c1 '&' ('not' (('not' c1) '&' c2))) by Th16
.= (('not' c1) '&' c2) 'or' (c1 '&' (('not' ('not' c1)) 'or' ('not' c2)))
.= (('not' c1) '&' c2) 'or' (c1 '&' (c1 'or' ('not' c2)))
.= c1 'or' (('not' c1) '&' c2) by Th25
.= c1 'or' c2 by Th26 ;
end;

theorem Th36: :: BINARITH:36
for b1, b2 being boolean set holds b1 'or' (b1 'xor' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
thus c1 'or' (c1 'xor' c2) = c1 'or' ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2)))
.= (c1 'or' (('not' c1) '&' c2)) 'or' (c1 '&' ('not' c2)) by Th20
.= (c1 'or' c2) 'or' (c1 '&' ('not' c2)) by Th26
.= (c1 'or' (c1 'or' c2)) '&' ((c1 'or' c2) 'or' ('not' c2)) by Th23
.= ((c1 'or' c1) 'or' c2) '&' ((c1 'or' c2) 'or' ('not' c2)) by Th20
.= (c1 'or' c2) '&' ((c1 'or' c2) 'or' ('not' c2)) by Th21
.= (c1 'or' c2) '&' (c1 'or' (c2 'or' ('not' c2))) by Th20
.= (c1 'or' c2) '&' (c1 'or' TRUE ) by Th18
.= TRUE '&' (c1 'or' c2) by Th19
.= c1 'or' c2 by MARGREL1:50 ;
end;

theorem Th37: :: BINARITH:37
for b1, b2 being boolean set holds b1 'or' (('not' b1)