:: BINARI_5 semantic presentation

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

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

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

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

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

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

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

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

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

:: deftheorem Def3 defines 'xnor' BINARI_5:def 3 :
for b1, b2 being boolean set holds b1 'xnor' b2 = 'not' (b1 'xor' b2);

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

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

theorem Th1: :: BINARI_5:1
for b1 being boolean set holds TRUE 'nand' b1 = 'not' b1 by MARGREL1:50;

theorem Th2: :: BINARI_5:2
for b1 being boolean set holds FALSE 'nand' b1 = TRUE
proof
let c1 be boolean set ;
thus FALSE 'nand' c1 = 'not' (FALSE '&' c1)
.= 'not' FALSE by MARGREL1:49
.= TRUE by MARGREL1:41 ;
end;

theorem Th3: :: BINARI_5:3
for b1 being boolean set holds
( b1 'nand' b1 = 'not' b1 & 'not' (b1 'nand' b1) = b1 ) by BINARITH:16;

theorem Th4: :: BINARI_5:4
for b1, b2 being boolean set holds 'not' (b1 'nand' b2) = b1 '&' b2 ;

theorem Th5: :: BINARI_5:5
for b1 being boolean set holds
( b1 'nand' ('not' b1) = TRUE & 'not' (b1 'nand' ('not' b1)) = FALSE )
proof
let c1 be boolean set ;
c1 'nand' ('not' c1) = 'not' (c1 '&' ('not' c1))
.= 'not' FALSE by MARGREL1:46
.= TRUE by MARGREL1:41 ;
hence ( c1 'nand' ('not' c1) = TRUE & 'not' (c1 'nand' ('not' c1)) = FALSE ) by MARGREL1:41;
end;

theorem Th6: :: BINARI_5:6
for b1, b2, b3 being boolean set holds b1 'nand' (b2 '&' b3) = 'not' ((b1 '&' b2) '&' b3) by MARGREL1:52;

theorem Th7: :: BINARI_5:7
for b1, b2, b3 being boolean set holds b1 'nand' (b2 '&' b3) = (b1 '&' b2) 'nand' b3 by MARGREL1:52;

theorem Th8: :: BINARI_5:8
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'or' b3) = ('not' (b1 '&' b2)) '&' ('not' (b1 '&' b3))
proof
let c1, c2, c3 be boolean set ;
thus c1 'nand' (c2 'or' c3) = 'not' (c1 '&' (c2 'or' c3))
.= 'not' ((c1 '&' c2) 'or' (c1 '&' c3)) by BINARITH:22
.= ('not' (c1 '&' c2)) '&' ('not' (c1 '&' c3)) by BINARITH:10 ;
end;

theorem Th9: :: BINARI_5:9
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'xor' b3) = (b1 '&' b2) 'eqv' (b1 '&' b3) by BINARITH:38;

theorem Th10: :: BINARI_5:10
for b1 being boolean set holds TRUE 'nor' b1 = FALSE
proof
let c1 be boolean set ;
TRUE 'nor' c1 = 'not' (TRUE 'or' c1)
.= 'not' TRUE by BINARITH:19 ;
hence TRUE 'nor' c1 = FALSE by MARGREL1:41;
end;

theorem Th11: :: BINARI_5:11
for b1 being boolean set holds FALSE 'nor' b1 = 'not' b1 by BINARITH:7;

theorem Th12: :: BINARI_5:12
for b1 being boolean set holds
( b1 'nor' b1 = 'not' b1 & 'not' (b1 'nor' b1) = b1 ) by BINARITH:21;

theorem Th13: :: BINARI_5:13
for b1, b2 being boolean set holds 'not' (b1 'nor' b2) = b1 'or' b2 ;

theorem Th14: :: BINARI_5:14
for b1 being boolean set holds
( b1 'nor' ('not' b1) = FALSE & 'not' (b1 'nor' ('not' b1)) = TRUE )
proof
let c1 be boolean set ;
c1 'nor' ('not' c1) = 'not' (c1 'or' ('not' c1))
.= 'not' TRUE by BINARITH:18
.= FALSE by MARGREL1:41 ;
hence ( c1 'nor' ('not' c1) = FALSE & 'not' (c1 'nor' ('not' c1)) = TRUE ) by MARGREL1:41;
end;

theorem Th15: :: BINARI_5:15
for b1, b2, b3 being boolean set holds b1 'nor' (b2 '&' b3) = ('not' (b1 'or' b2)) 'or' ('not' (b1 'or' b3))
proof
let c1, c2, c3 be boolean set ;
c1 'nor' (c2 '&' c3) = 'not' (c1 'or' (c2 '&' c3))
.= 'not' ((c1 'or' c2) '&' (c1 'or' c3)) by BINARITH:23
.= ('not' (c1 'or' c2)) 'or' ('not' (c1 'or' c3)) by BINARITH:9 ;
hence c1 'nor' (c2 '&' c3) = ('not' (c1 'or' c2)) 'or' ('not' (c1 'or' c3)) ;
end;

theorem Th16: :: BINARI_5:16
for b1, b2, b3 being boolean set holds b1 'nor' (b2 'or' b3) = 'not' ((b1 'or' b2) 'or' b3) by BINARITH:20;

theorem Th17: :: BINARI_5:17
for b1 being boolean set holds TRUE 'xnor' b1 = b1
proof
let c1 be boolean set ;
TRUE 'xnor' c1 = 'not' (TRUE 'xor' c1)
.= 'not' ('not' c1) by BINARITH:13 ;
hence TRUE 'xnor' c1 = c1 ;
end;

theorem Th18: :: BINARI_5:18
for b1 being boolean set holds FALSE 'xnor' b1 = 'not' b1 by BINARITH:14;

theorem Th19: :: BINARI_5:19
for b1 being boolean set holds
( b1 'xnor' b1 = TRUE & 'not' (b1 'xnor' b1) = FALSE )
proof
let c1 be boolean set ;
c1 'xnor' c1 = 'not' (c1 'xor' c1)
.= 'not' ((('not' c1) '&' c1) 'or' (c1 '&' ('not' c1))) by BINARITH:def 2
.= 'not' (FALSE 'or' (c1 '&' ('not' c1))) by MARGREL1:46
.= 'not' (FALSE 'or' FALSE ) by MARGREL1:46
.= 'not' FALSE by BINARITH:7
.= TRUE by MARGREL1:41 ;
hence ( c1 'xnor' c1 = TRUE & 'not' (c1 'xnor' c1) = FALSE ) by MARGREL1:41;
end;

theorem Th20: :: BINARI_5:20
for b1, b2 being boolean set holds 'not' (b1 'xnor' b2) = b1 'xor' b2 ;

theorem Th21: :: BINARI_5:21
for b1 being boolean set holds
( b1 'xnor' ('not' b1) = FALSE & 'not' (b1 'xnor' ('not' b1)) = TRUE )
proof
let c1 be boolean set ;
c1 'xnor' ('not' c1) = 'not' (c1 'xor' ('not' c1))
.= 'not' TRUE by BINARITH:17
.= FALSE by MARGREL1:41 ;
hence ( c1 'xnor' ('not' c1) = FALSE & 'not' (c1 'xnor' ('not' c1)) = TRUE ) by MARGREL1:41;
end;

theorem Th22: :: BINARI_5:22
for b1, b2, b3 being boolean set holds
( b1 '<' b2 'imp' b3 iff b1 '&' b2 '<' b3 )
proof
let c1, c2, c3 be boolean set ;
E1: ( c1 '<' c2 'imp' c3 implies c1 '&' c2 '<' c3 )
proof
assume c1 '<' c2 'imp' c3 ;
then E2: c1 'imp' (c2 'imp' c3) = TRUE by BVFUNC_1:def 3;
c1 'imp' (c2 'imp' c3) = ('not' c1) 'or' (c2 'imp' c3)
.= ('not' c1) 'or' (('not' c2) 'or' c3)
.= (('not' c1) 'or' ('not' c2)) 'or' c3 by BINARITH:20
.= ('not' (c1 '&' c2)) 'or' c3 by BINARITH:9
.= (c1 '&' c2) 'imp' c3 ;
hence c1 '&' c2 '<' c3 by E2, BVFUNC_1:def 3;
end;
( c1 '&' c2 '<' c3 implies c1 '<' c2 'imp' c3 )
proof
assume c1 '&' c2 '<' c3 ;
then E2: (c1 '&' c2) 'imp' c3 = TRUE by BVFUNC_1:def 3;
(c1 '&' c2) 'imp' c3 = ('not' (c1 '&' c2)) 'or' c3
.= (('not' c1) 'or' ('not' c2)) 'or' c3 by BINARITH:9
.= ('not' c1) 'or' (('not' c2) 'or' c3) by BINARITH:20
.= ('not' c1) 'or' (c2 'imp' c3)
.= c1 'imp' (c2 'imp' c3) ;
hence c1 '<' c2 'imp' c3 by E2, BVFUNC_1:def 3;
end;
hence ( c1 '<' c2 'imp' c3 iff c1 '&' c2 '<' c3 ) by E1;
end;

theorem Th23: :: BINARI_5:23
for b1, b2 being boolean set holds b1 'eqv' b2 = (b1 'imp' b2) '&' (b2 'imp' b1)
proof
let c1, c2 be boolean set ;
thus c1 'eqv' c2 = 'not' (c1 'xor' c2)
.= 'not' ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) by BINARITH:def 2
.= ('not' (('not' c1) '&' c2)) '&' ('not' (c1 '&' ('not' c2))) by BINARITH:10
.= (('not' ('not' c1)) 'or' ('not' c2)) '&' ('not' (c1 '&' ('not' c2))) by BINARITH:9
.= (('not' ('not' c1)) 'or' ('not' c2)) '&' (('not' c1) 'or' ('not' ('not' c2))) by BINARITH:9
.= (c1 'or' ('not' c2)) '&' (('not' c1) 'or' ('not' ('not' c2)))
.= (c1 'or' ('not' c2)) '&' (('not' c1) 'or' c2)
.= ((c1 'or' ('not' c2)) '&' ('not' c1)) 'or' ((c1 'or' ('not' c2)) '&' c2) by BINARITH:22
.= ((('not' c1) '&' c1) 'or' (('not' c1) '&' ('not' c2))) 'or' (c2 '&' (c1 'or' ('not' c2))) by BINARITH:22
.= ((('not' c1) '&' c1) 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' (c2 '&' ('not' c2))) by BINARITH:22
.= (FALSE 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' (c2 '&' ('not' c2))) by MARGREL1:46
.= (FALSE 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' FALSE ) by MARGREL1:46
.= (('not' c1) '&' ('not' c2)) 'or' ((c2 '&' c1) 'or' FALSE ) by BINARITH:7
.= (('not' c1) '&' ('not' c2)) 'or' (c2 '&' c1) by BINARITH:7
.= ((('not' c1) '&' ('not' c2)) 'or' c2) '&' ((('not' c1) '&' ('not' c2)) 'or' c1) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' (c2 'or' ('not' c2))) '&' (c1 'or' (('not' c1) '&' ('not' c2))) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' (c2 'or' ('not' c2))) '&' ((c1 'or' ('not' c1)) '&' (c1 'or' ('not' c2))) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' TRUE ) '&' ((c1 'or' ('not' c1)) '&' (c1 'or' ('not' c2))) by BINARITH:18
.= ((c2 'or' ('not' c1)) '&' TRUE ) '&' (TRUE '&' (c1 'or' ('not' c2))) by BINARITH:18
.= (c2 'or' ('not' c1)) '&' (TRUE '&' (c1 'or' ('not' c2))) by MARGREL1:50
.= (c2 'or' ('not' c1)) '&' (c1 'or' ('not' c2)) by MARGREL1:50
.= (c1 'imp' c2) '&' (c1 'or' ('not' c2))
.= (c1 'imp' c2) '&' (c2 'imp' c1) ;
end;

theorem Th24: :: BINARI_5:24
for b1, b2 being boolean set holds
( b1 'eqv' b2 = TRUE iff ( b1 'imp' b2 = TRUE & b2 'imp' b1 = TRUE ) )
proof
let c1, c2 be boolean set ;
E3: ( c1 'eqv' c2 = TRUE implies ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) )
proof
assume c1 'eqv' c2 = TRUE ;
then (c1 'imp' c2) '&' (c2 'imp' c1) = TRUE by Th23;
hence ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by MARGREL1:45;
end;
( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE implies c1 'eqv' c2 = TRUE )
proof
assume ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ;
then (c1 'imp' c2) '&' (c2 'imp' c1) = TRUE by MARGREL1:def 17;
hence c1 'eqv' c2 = TRUE by Th23;
end;
hence ( c1 'eqv' c2 = TRUE iff ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ) by E3;
end;

theorem Th25: :: BINARI_5:25
for b1, b2 being boolean set holds
( b1 'imp' b2 = TRUE & b2 'imp' b1 = TRUE implies b1 = b2 )
proof
let c1, c2 be boolean set ;
assume E3: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ;
now
per cases not ( not ( c1 = FALSE & c2 = FALSE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = TRUE & c2 = FALSE ) & not ( c1 = TRUE & c2 = TRUE ) ) by MARGREL1:39;
case ( c1 = FALSE & c2 = FALSE ) ;
hence c1 = c2 ;
end;
case E4: ( c1 = FALSE & c2 = TRUE ) ;
c2 'imp' c1 = ('not' c2) 'or' c1
.= FALSE 'or' FALSE by E4, MARGREL1:41
.= FALSE by BINARITH:7 ;
hence not verum by E3;
end;
case E4: ( c1 = TRUE & c2 = FALSE ) ;
c1 'imp' c2 = ('not' c1) 'or' c2
.= FALSE 'or' FALSE by E4, MARGREL1:41
.= FALSE by BINARITH:7 ;
hence not verum by E3;
end;
case ( c1 = TRUE & c2 = TRUE ) ;
hence c1 = c2 ;
end;
end;
end;
hence c1 = c2 ;
end;

theorem Th26: :: BINARI_5:26
for b1, b2, b3 being boolean set holds
( b1 'imp' b2 = TRUE & b2 'imp' b3 = TRUE implies b1 'imp' b3 = TRUE )
proof
let c1, c2, c3 be boolean set ;
assume E4: ( c1 'imp' c2 = TRUE & c2 'imp' c3 = TRUE ) ;
E5: now
assume E6: c1 = TRUE ;
E7: c1 'imp' c2 = ('not' c1) 'or' c2
.= FALSE 'or' c2 by E6, MARGREL1:41
.= c2 by BINARITH:7 ;
c2 'imp' c3 = ('not' c2) 'or' c3
.= FALSE 'or' c3 by E4, E7, MARGREL1:41
.= c3 by BINARITH:7 ;
then c1 'imp' c3 = ('not' c1) 'or' TRUE by E4;
hence c1 'imp' c3 = TRUE by BINARITH:19;
end;
now
assume E6: c1 <> TRUE ;
c1 'imp' c3 = ('not' c1) 'or' c3
.= ('not' FALSE ) 'or' c3 by E6, MARGREL1:39
.= TRUE 'or' c3 by MARGREL1:41 ;
hence c1 'imp' c3 = TRUE by BINARITH:19;
end;
hence c1 'imp' c3 = TRUE by E5;
end;

theorem Th27: :: BINARI_5:27
for b1, b2, b3 being boolean set holds
( b1 'eqv' b2 = TRUE & b2 'eqv' b3 = TRUE implies b1 'eqv' b3 = TRUE )
proof
let c1, c2, c3 be boolean set ;
assume E4: ( c1 'eqv' c2 = TRUE & c2 'eqv' c3 = TRUE ) ;
then E5: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by Th24;
E6: ( c2 'imp' c3 = TRUE & c3 'imp' c2 = TRUE ) by E4, Th24;
then E7: c1 'imp' c3 = TRUE by E5, Th26;
c3 'imp' c1 = TRUE by E5, E6, Th26;
hence c1 'eqv' c3 = TRUE by E7, Th24;
end;

theorem Th28: :: BINARI_5:28
for b1, b2 being boolean set holds b1 'imp' b2 = ('not' b2) 'imp' ('not' b1) ;

theorem Th29: :: BINARI_5:29
for b1, b2 being boolean set holds b1 'eqv' b2 = ('not' b1) 'eqv' ('not' b2)
proof
let c1, c2 be boolean set ;
thus ('not' c1) 'eqv' ('not' c2) = (('not' c1) 'imp' ('not' c2)) '&' (('not' c2) 'imp' ('not' c1)) by Th23
.= (c2 'imp' c1) '&' (('not' c2) 'imp' ('not' c1))
.= (c2 'imp' c1) '&' (c1 'imp' c2)
.= c1 'eqv' c2 by Th23 ;
end;

theorem Th30: :: BINARI_5:30
for b1, b2, b3, b4 being boolean set holds
( b1 'eqv' b2 = TRUE & b3 'eqv' b4 = TRUE implies (b1 '&' b3) 'eqv' (b2 '&' b4) = TRUE )
proof
let c1, c2, c3, c4 be boolean set ;
assume E4: ( c1 'eqv' c2 = TRUE & c3 'eqv' c4 = TRUE ) ;
then E5: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by Th24;
E6: ( c3 'imp' c4 = TRUE & c4 'imp' c3 = TRUE ) by E4, Th24;
E7: ('not' c1) 'or' c2 = TRUE by E5;
E8: ('not' c2) 'or' c1 = TRUE by E5;
E9: ('not' c3) 'or' c4 = TRUE by E6;
E10: ('not' c4) 'or' c3 = TRUE by E6;
(c1 '&' c3) 'eqv' (c2 '&' c4) = ((c1 '&' c3) 'imp' (c2 '&' c4)) '&' ((c2 '&' c4) 'imp' (c1 '&' c3)) by Th23
.= (('not' (c1 '&' c3)) 'or' (c2 '&' c4)) '&' ((c2 '&' c4) 'imp' (c1 '&' c3))
.= (('not' (c1 '&' c3)) 'or' (c2 '&' c4)) '&' (('not' (c2 '&' c4)) 'or' (c1 '&' c3))
.= ((('not' c1) 'or' ('not' c3)) 'or' (c2 '&' c4)) '&' (('not' (c2 '&' c4)) 'or' (c1 '&' c3)) by BINARITH:9
.= ((('not' c1) 'or' ('not' c3)) 'or' (c2 '&' c4)) '&' ((('not' c2) 'or' ('not' c4)) 'or' (c1 '&' c3)) by BINARITH:9
.= (((('not' c1) 'or' ('not' c3)) 'or' c2) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' ((('not' c2) 'or' ('not' c4)) 'or' (c1 '&' c3)) by BINARITH:23
.= (((('not' c1) 'or' ('not' c3)) 'or' c2) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:23
.= (((('not' c1) 'or' c2) 'or' ('not' c3)) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:20
.= (TRUE '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by E7, BINARITH:19
.= ((('not' c1) 'or' ('not' c3)) 'or' c4) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by MARGREL1:50
.= (('not' c1) 'or' (('not' c3) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:20
.= TRUE '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by E9, BINARITH:19
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3) by MARGREL1:50
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' (('not' c2) 'or' (('not' c4) 'or' c3)) by BINARITH:20
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' TRUE by E10, BINARITH:19
.= (('not' c2) 'or' ('not' c4)) 'or' c1 by MARGREL1:50
.= ('not' c4) 'or' (('not' c2) 'or' c1) by BINARITH:20
.= TRUE by E8, BINARITH:19 ;
hence (c1 '&' c3) 'eqv' (c2 '&' c4) = TRUE ;
end;

theorem Th31: :: BINARI_5:31
for b1, b2, b3, b4 being boolean set holds
( b1 'eqv' b2 = TRUE & b3 'eqv' b4 = TRUE implies (b1 'imp' b3) 'eqv' (b2 'imp' b4) = TRUE )
proof
let c1, c2, c3, c4 be boolean set ;
assume E4: ( c1 'eqv' c2 = TRUE & c3 'eqv' c4 = TRUE ) ;
then E5: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by Th24;
E6: ( c3 'imp' c4 = TRUE & c4 'imp' c3 = TRUE ) by E4, Th24;
E7: ('not' c1) 'or' c2 = TRUE by E5;
E8: ('not' c2) 'or' c1 = TRUE by E5;
E9: ('not' c3) 'or' c4 = TRUE by E6;
E10: ('not' c4) 'or' c3 = TRUE by E6;
(c1 'imp' c3) 'eqv' (c2 'imp' c4) = ((c1 'imp' c3) 'imp' (c2 'imp' c4)) '&' ((c2 'imp' c4) 'imp' (c1 'imp' c3)) by Th23
.= (('not' (c1 'imp' c3)) 'or' (c2 'imp' c4)) '&' ((c2 'imp' c4) 'imp' (c1 'imp' c3))
.= (('not' (c1 'imp' c3)) 'or' (c2 'imp' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3))
.= (('not' (('not' c1) 'or' c3)) 'or' (c2 'imp' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3))
.= (('not' (('not' c1) 'or' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3))
.= (('not' (('not' c1) 'or' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (('not' c2) 'or' c4)) 'or' (c1 'imp' c3))
.= (('not' (('not' c1) 'or' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (('not' c2) 'or' c4)) 'or' (('not' c1) 'or' c3))
.= ((('not' ('not' c1)) '&' ('not' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (('not' c2) 'or' c4)) 'or' (('not' c1) 'or' c3)) by BINARITH:10
.= ((('not' ('not' c1)) '&' ('not' c3)) 'or' (('not' c2) 'or' c4)) '&' ((('not' ('not' c2)) '&' ('not' c4)) 'or' (('not' c1) 'or' c3)) by BINARITH:10
.= ((c1 '&' ('not' c3)) 'or' (('not' c2) 'or' c4)) '&' ((('not' ('not' c2)) '&' ('not' c4)) 'or' (('not' c1) 'or' c3))
.= ((c1 '&' ('not' c3)) 'or' (('not' c2) 'or' c4)) '&' ((c2 '&' ('not' c4)) 'or' (('not' c1) 'or' c3))
.= ((c1 'or' (('not' c2) 'or' c4)) '&' (('not' c3) 'or'