:: BVFUNC25 semantic presentation

begin


theorem :: BVFUNC25:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'imp' b) = a '&' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'imp' b) = a '&' ('not' b)
thus  'not' (a 'imp' b) = 'not' (('not' a) 'or' b) by BVFUNC_4:8
.= ('not' ('not' a)) '&' ('not' b) by BVFUNC_1:13
.= a '&' ('not' b) ; ::_thesis: verum
end;

theorem Th2: :: BVFUNC25:2
for Y being non empty set
for b, a being Function of Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for b, a being Function of Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
let b, a be Function of Y,BOOLEAN; ::_thesis: (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
(('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = ('not' (('not' b) 'imp' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8
.= ('not' (('not' ('not' b)) 'or' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8
.= (('not' b) '&' ('not' ('not' a))) 'or' (a 'imp' b) by BVFUNC_1:13
.= (('not' b) '&' a) 'or' (('not' a) 'or' b) by BVFUNC_4:8
.= ((('not' b) '&' a) 'or' ('not' a)) 'or' b by BVFUNC_1:8
.= ((('not' b) 'or' ('not' a)) '&' (a 'or' ('not' a))) 'or' b by BVFUNC_1:11
.= ((('not' b) 'or' ('not' a)) '&' (I_el Y)) 'or' b by BVFUNC_4:6
.= (('not' b) 'or' ('not' a)) 'or' b by BVFUNC_1:6
.= ('not' a) 'or' (('not' b) 'or' b) by BVFUNC_1:8
.= ('not' a) 'or' (I_el Y) by BVFUNC_4:6 ;
hence  (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem Th3: :: BVFUNC25:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = ('not' b) 'imp' ('not' a)
 (a 'imp' b) 'imp' (('not' b) 'imp' ('not' a)) = I_el Y by BVFUNC_5:32;
then A1: a 'imp' b '<' ('not' b) 'imp' ('not' a) by BVFUNC_1:16;
 (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by Th2;
then  ('not' b) 'imp' ('not' a) '<' a 'imp' b by BVFUNC_1:16;
hence  a 'imp' b = ('not' b) 'imp' ('not' a) by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC25:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = ('not' a) 'eqv' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = ('not' a) 'eqv' ('not' b)
thus ('not' a) 'eqv' ('not' b) = (('not' a) 'imp' ('not' b)) '&' (('not' b) 'imp' ('not' a)) by BVFUNC_4:7
.= (b 'imp' a) '&' (('not' b) 'imp' ('not' a)) by Th3
.= (b 'imp' a) '&' (a 'imp' b) by Th3
.= a 'eqv' b by BVFUNC_4:7 ; ::_thesis: verum
end;

theorem Th5: :: BVFUNC25:5
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'imp' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = a 'imp' (a '&' b)
a 'imp' (a '&' b) = ('not' a) 'or' (a '&' b) by BVFUNC_4:8
.= (('not' a) 'or' a) '&' (('not' a) 'or' b) by BVFUNC_1:11
.= (I_el Y) '&' (('not' a) 'or' b) by BVFUNC_4:6
.= ('not' a) 'or' b by BVFUNC_1:6 ;
hence  a 'imp' b = a 'imp' (a '&' b) by BVFUNC_4:8; ::_thesis: verum
end;

theorem :: BVFUNC25:6
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' b) 'imp' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a 'or' b) 'imp' (a '&' b)
thus (a 'or' b) 'imp' (a '&' b) = (a 'imp' (a '&' b)) '&' (b 'imp' (a '&' b)) by BVFUNC_7:5
.= (a 'imp' b) '&' (b 'imp' (a '&' b)) by Th5
.= (a 'imp' b) '&' (b 'imp' a) by Th5
.= a 'eqv' b by BVFUNC_4:7 ; ::_thesis: verum
end;

theorem :: BVFUNC25:7
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'eqv' ('not' a) = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'eqv' ('not' a) = O_el Y
thus a 'eqv' ('not' a) = (a 'imp' ('not' a)) '&' (('not' a) 'imp' a) by BVFUNC_4:7
.= (('not' a) 'or' ('not' a)) '&' (('not' a) 'imp' a) by BVFUNC_4:8
.= ('not' a) '&' (('not' ('not' a)) 'or' a) by BVFUNC_4:8
.= O_el Y by BVFUNC_4:5 ; ::_thesis: verum
end;

theorem :: BVFUNC25:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'imp' c) = b 'imp' (a 'imp' c)
thus a 'imp' (b 'imp' c) = ('not' a) 'or' (b 'imp' c) by BVFUNC_4:8
.= ('not' a) 'or' (('not' b) 'or' c) by BVFUNC_4:8
.= ('not' b) 'or' (('not' a) 'or' c) by BVFUNC_1:8
.= ('not' b) 'or' (a 'imp' c) by BVFUNC_4:8
.= b 'imp' (a 'imp' c) by BVFUNC_4:8 ; ::_thesis: verum
end;

theorem :: BVFUNC25:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'imp' c) = (a 'imp' b) 'imp' (a 'imp' c)
thus (a 'imp' b) 'imp' (a 'imp' c) = (a 'imp' b) 'imp' (('not' a) 'or' c) by BVFUNC_4:8
.= ('not' (a 'imp' b)) 'or' (('not' a) 'or' c) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' (('not' a) 'or' c) by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' b)) 'or' (('not' a) 'or' c) by BVFUNC_1:13
.= ((a '&' ('not' b)) 'or' ('not' a)) 'or' c by BVFUNC_1:8
.= ((a 'or' ('not' a)) '&' (('not' b) 'or' ('not' a))) 'or' c by BVFUNC_1:11
.= ((I_el Y) '&' (('not' b) 'or' ('not' a))) 'or' c by BVFUNC_4:6
.= (('not' a) 'or' ('not' b)) 'or' c by BVFUNC_1:6
.= ('not' a) 'or' (('not' b) 'or' c) by BVFUNC_1:8
.= ('not' a) 'or' (b 'imp' c) by BVFUNC_4:8
.= a 'imp' (b 'imp' c) by BVFUNC_4:8 ; ::_thesis: verum
end;

theorem :: BVFUNC25:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = a 'xor' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = a 'xor' ('not' b)
 'not' (a 'xor' b) = 'not' ('not' (a 'eqv' b)) by BVFUNC_8:12;
hence  a 'eqv' b = a 'xor' ('not' b) by BVFUNC_8:17; ::_thesis: verum
end;

theorem :: BVFUNC25:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
A1: (a '&' b) 'xor' (a '&' c) = (('not' (a '&' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c))) by BVFUNC_4:9
.= ((('not' a) 'or' ('not' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c))) by BVFUNC_1:14
.= ((a '&' c) '&' (('not' a) 'or' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c))) by BVFUNC_1:14
.= (((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c))) by BVFUNC_1:12
.= (((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' (((a '&' b) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' c))) by BVFUNC_1:12
.= ((a '&' c) '&' ('not' a)) 'or' (((a '&' c) '&' ('not' b)) 'or' (((a '&' b) '&' ('not' c)) 'or' ((a '&' b) '&' ('not' a)))) by BVFUNC_1:8
.= ((a '&' c) '&' ('not' a)) 'or' ((((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' b) '&' ('not' a))) by BVFUNC_1:8
.= (((a '&' c) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' a))) 'or' (((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))) by BVFUNC_1:8 ;
A2: ((c '&' a) '&' ('not' a)) 'or' ((b '&' a) '&' ('not' a)) = (c '&' (a '&' ('not' a))) 'or' ((b '&' a) '&' ('not' a)) by BVFUNC_1:4
.= (c '&' (a '&' ('not' a))) 'or' (b '&' (a '&' ('not' a))) by BVFUNC_1:4
.= (c '&' (O_el Y)) 'or' (b '&' (a '&' ('not' a))) by BVFUNC_4:5
.= (c '&' (O_el Y)) 'or' (b '&' (O_el Y)) by BVFUNC_4:5
.= (O_el Y) 'or' (b '&' (O_el Y)) by BVFUNC_1:5
.= (O_el Y) 'or' (O_el Y) by BVFUNC_1:5
.= O_el Y ;
a '&' (b 'xor' c) = a '&' ((('not' b) '&' c) 'or' (b '&' ('not' c))) by BVFUNC_4:9
.= (a '&' (('not' b) '&' c)) 'or' (a '&' (b '&' ('not' c))) by BVFUNC_1:12
.= ((a '&' c) '&' ('not' b)) 'or' (a '&' (b '&' ('not' c))) by BVFUNC_1:4
.= ((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c)) by BVFUNC_1:4 ;
hence  a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c) by A1, A2, BVFUNC_1:9; ::_thesis: verum
end;

theorem :: BVFUNC25:12
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = 'not' (a 'xor' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = 'not' (a 'xor' b)
 'not' (a 'xor' b) = 'not' ('not' (a 'eqv' b)) by BVFUNC_8:12;
hence  a 'eqv' b = 'not' (a 'xor' b) ; ::_thesis: verum
end;

theorem :: BVFUNC25:13
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' a = O_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' a = O_el Y
thus a 'xor' a = (('not' a) '&' a) 'or' (a '&' ('not' a)) by BVFUNC_4:9
.= O_el Y by BVFUNC_4:5 ; ::_thesis: verum
end;

theorem :: BVFUNC25:14
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' ('not' a) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' ('not' a) = I_el Y
thus a 'xor' ('not' a) = (('not' a) '&' ('not' a)) 'or' (a '&' ('not' ('not' a))) by BVFUNC_4:9
.= I_el Y by BVFUNC_4:6 ; ::_thesis: verum
end;

theorem :: BVFUNC25:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a
(a 'imp' b) 'imp' (b 'imp' a) = (('not' a) 'or' b) 'imp' (b 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' b) 'imp' (('not' b) 'or' a) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' (('not' b) 'or' a) by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' b)) 'or' (('not' b) 'or' a) by BVFUNC_1:13
.= ((a '&' ('not' b)) 'or' ('not' b)) 'or' a by BVFUNC_1:8
.= ((a 'or' ('not' b)) '&' (('not' b) 'or' ('not' b))) 'or' a by BVFUNC_1:11
.= ((a 'or' ('not' b)) 'or' a) '&' (('not' b) 'or' a) by BVFUNC_1:11
.= (('not' b) 'or' (a 'or' a)) '&' (('not' b) 'or' a) by BVFUNC_1:8
.= ('not' b) 'or' a ;
hence  (a 'imp' b) 'imp' (b 'imp' a) = b 'imp' a by BVFUNC_4:8; ::_thesis: verum
end;

theorem Th16: :: BVFUNC25:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
 a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_4:9;
hence  (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_8:13; ::_thesis: verum
end;

theorem Th17: :: BVFUNC25:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (a 'or' ('not' b))
thus (a '&' b) 'or' (('not' a) '&' ('not' b)) = (('not' a) 'or' b) '&' (('not' ('not' a)) 'or' ('not' b)) by Th16
.= (('not' a) 'or' b) '&' (a 'or' ('not' b)) ; ::_thesis: verum
end;

theorem :: BVFUNC25:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c
A1: (a 'xor' b) 'xor' c = ((('not' a) '&' b) 'or' (a '&' ('not' b))) 'xor' c by BVFUNC_4:9
.= (('not' ((('not' a) '&' b) 'or' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_4:9
.= ((('not' (('not' a) '&' b)) '&' ('not' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:13
.= (((('not' ('not' a)) 'or' ('not' b)) '&' ('not' (a '&' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:14
.= (((a 'or' ('not' b)) '&' (('not' a) 'or' ('not' ('not' b)))) '&' c) 'or' (((('not' a) '&' b) 'or' (a '&' ('not' b))) '&' ('not' c)) by BVFUNC_1:14
.= (((a 'or' ('not' b)) '&' (('not' a) 'or' b)) '&' c) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by BVFUNC_1:12
.= (((a '&' b) 'or' (('not' a) '&' ('not' b))) '&' c) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by Th17
.= (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' c)) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) by BVFUNC_1:12
.= (((a '&' b) '&' c) 'or' (((a '&' ('not' b)) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' ('not' c)))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8
.= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ;
a 'xor' (b 'xor' c) = (('not' a) '&' (b 'xor' c)) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9
.= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' (b 'xor' c))) by BVFUNC_4:9
.= (('not' a) '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_4:9
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ('not' ((('not' b) '&' c) 'or' (b '&' ('not' c))))) by BVFUNC_1:12
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' (('not' (('not' b) '&' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:13
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((('not' ('not' b)) 'or' ('not' c)) '&' ('not' (b '&' ('not' c))))) by BVFUNC_1:14
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b 'or' ('not' c)) '&' (('not' b) 'or' ('not' ('not' c))))) by BVFUNC_1:14
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' (a '&' ((b '&' c) 'or' (('not' b) '&' ('not' c)))) by Th17
.= ((('not' a) '&' (('not' b) '&' c)) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:12
.= (((('not' a) '&' ('not' b)) '&' c) 'or' (('not' a) '&' (b '&' ('not' c)))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((a '&' (b '&' c)) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((('not' a) '&' ('not' b)) '&' c) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' (((a '&' b) '&' c) 'or' (a '&' (('not' b) '&' ('not' c)))) by BVFUNC_1:4
.= (((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' (((('not' a) '&' b) '&' ('not' c)) 'or' ((('not' a) '&' ('not' b)) '&' c)) by BVFUNC_1:4
.= ((((a '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' ('not' c))) 'or' ((('not' a) '&' ('not' b)) '&' c) by BVFUNC_1:8 ;
hence  a 'xor' (b 'xor' c) = (a 'xor' b) 'xor' c by A1; ::_thesis: verum
end;

theorem :: BVFUNC25:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c
A1: (a 'eqv' b) 'eqv' c = ((a 'eqv' b) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7
.= (((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' (a 'eqv' b)) by BVFUNC_4:7
.= (((a 'imp' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:7
.= (((('not' a) 'or' b) '&' (b 'imp' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
.= (((('not' a) 'or' b) '&' (('not' b) 'or' a)) 'imp' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
.= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (c 'imp' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
.= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((a 'imp' b) '&' (b 'imp' a))) by BVFUNC_4:8
.= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (b 'imp' a))) by BVFUNC_4:8
.= (('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_4:8
.= ((('not' (('not' a) 'or' b)) 'or' ('not' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:14
.= (((('not' ('not' a)) '&' ('not' b)) 'or' ('not' (('not' b) 'or' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:13
.= (((a '&' ('not' b)) 'or' (('not' ('not' b)) '&' ('not' a))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:13
.= (((a 'or' b) '&' (('not' a) 'or' ('not' b))) 'or' c) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by Th16
.= (((a 'or' b) 'or' c) '&' ((('not' a) 'or' ('not' b)) 'or' c)) '&' (('not' c) 'or' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) by BVFUNC_1:11
.= (((a 'or' b) 'or' c) '&' ((('not' a) 'or' ('not' b)) 'or' c)) '&' (((a 'or' ('not' b)) 'or' ('not' c)) '&' ((('not' a) 'or' b) 'or' ('not' c))) by BVFUNC_1:11
.= (((a 'or' b) 'or' c) '&' (((a 'or' ('not' b)) 'or' ('not' c)) '&' ((('not' a) 'or' b) 'or' ('not' c)))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4
.= ((((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4 ;
a 'eqv' (b 'eqv' c) = (a 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7
.= (a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' ((b 'eqv' c) 'imp' a) by BVFUNC_4:7
.= (a 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:7
.= (('not' a) 'or' ((b 'imp' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (c 'imp' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'imp' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (c 'imp' b)) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' b) 'or' c) '&' (('not' c) 'or' b)) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (('not' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) 'or' a) by BVFUNC_4:8
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' ((('not' (('not' b) 'or' c)) 'or' ('not' (('not' c) 'or' b))) 'or' a) by BVFUNC_1:14
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((('not' ('not' b)) '&' ('not' c)) 'or' ('not' (('not' c) 'or' b))) 'or' a) by BVFUNC_1:13
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b '&' ('not' c)) 'or' (('not' ('not' c)) '&' ('not' b))) 'or' a) by BVFUNC_1:13
.= (('not' a) 'or' ((('not' b) 'or' c) '&' (('not' c) 'or' b))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by Th16
.= ((('not' a) 'or' (('not' b) 'or' c)) '&' (('not' a) 'or' (('not' c) 'or' b))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:11
.= (((('not' a) 'or' ('not' b)) 'or' c) '&' (('not' a) 'or' (b 'or' ('not' c)))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:8
.= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((b 'or' c) '&' (('not' b) 'or' ('not' c))) 'or' a) by BVFUNC_1:8
.= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((a 'or' (b 'or' c)) '&' (a 'or' (('not' b) 'or' ('not' c)))) by BVFUNC_1:11
.= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((a 'or' b) 'or' c) '&' (a 'or' (('not' b) 'or' ('not' c)))) by BVFUNC_1:8
.= (((('not' a) 'or' ('not' b)) 'or' c) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' (((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) by BVFUNC_1:8
.= ((((a 'or' b) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c))) '&' ((('not' a) 'or' b) 'or' ('not' c))) '&' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:4 ;
hence  a 'eqv' (b 'eqv' c) = (a 'eqv' b) 'eqv' c by A1; ::_thesis: verum
end;

theorem :: BVFUNC25:20
for Y being non empty set
for a being Function of Y,BOOLEAN holds ('not' ('not' a)) 'imp' a = I_el Y by BVFUNC_5:7;

theorem :: BVFUNC25:21
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) '&' a) 'imp' b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' a) 'imp' b = I_el Y
 ((a 'imp' b) '&' a) 'imp' b = (a '&' b) 'imp' b by BVFUNC_7:10;
hence  ((a 'imp' b) '&' a) 'imp' b = I_el Y by BVFUNC_6:40; ::_thesis: verum
end;

theorem Th22: :: BVFUNC25:22
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'imp' a) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (('not' a) 'imp' a) = I_el Y
a 'imp' (('not' a) 'imp' a) = ('not' a) 'or' (('not' a) 'imp' a) by BVFUNC_4:8
.= ('not' a) 'or' (('not' ('not' a)) 'or' a) by BVFUNC_4:8
.= ('not' a) 'or' a ;
hence  a 'imp' (('not' a) 'imp' a) = I_el Y by BVFUNC_4:6; ::_thesis: verum
end;

theorem :: BVFUNC25:23
for Y being non empty set
for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'imp' a) 'eqv' a = I_el Y
(('not' a) 'imp' a) 'eqv' a = ((('not' a) 'imp' a) 'imp' a) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_4:7
.= (I_el Y) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_5:11
.= a 'imp' (('not' a) 'imp' a) by BVFUNC_1:6 ;
hence  (('not' a) 'imp' a) 'eqv' a = I_el Y by Th22; ::_thesis: verum
end;

theorem :: BVFUNC25:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a 'imp' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a 'imp' b) = I_el Y
a 'or' (a 'imp' b) = a 'or' (('not' a) 'or' b) by BVFUNC_4:8
.= (a 'or' ('not' a)) 'or' b by BVFUNC_1:8
.= (I_el Y) 'or' b by BVFUNC_4:6 ;
hence  a 'or' (a 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:25
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (c 'imp' a) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (c 'imp' a) = I_el Y
(a 'imp' b) 'or' (c 'imp' a) = (('not' a) 'or' b) 'or' (c 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' b) 'or' (('not' c) 'or' a) by BVFUNC_4:8
.= ('not' c) 'or' (a 'or' (('not' a) 'or' b)) by BVFUNC_1:8
.= ('not' c) 'or' ((a 'or' ('not' a)) 'or' b) by BVFUNC_1:8
.= ('not' c) 'or' ((I_el Y) 'or' b) by BVFUNC_4:6
.= ('not' c) 'or' (I_el Y) by BVFUNC_1:10 ;
hence  (a 'imp' b) 'or' (c 'imp' a) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y
(a 'imp' b) 'or' (('not' a) 'imp' b) = (('not' a) 'or' b) 'or' (('not' a) 'imp' b) by BVFUNC_4:8
.= (('not' a) 'or' b) 'or' (('not' ('not' a)) 'or' b) by BVFUNC_4:8
.= b 'or' (('not' a) 'or' (a 'or' b)) by BVFUNC_1:8
.= b 'or' ((('not' a) 'or' a) 'or' b) by BVFUNC_1:8
.= b 'or' ((I_el Y) 'or' b) by BVFUNC_4:6
.= b 'or' (I_el Y) by BVFUNC_1:10 ;
hence  (a 'imp' b) 'or' (('not' a) 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y
(a 'imp' b) 'or' (a 'imp' ('not' b)) = (('not' a) 'or' b) 'or' (a 'imp' ('not' b)) by BVFUNC_4:8
.= (('not' a) 'or' b) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:8
.= ('not' a) 'or' (b 'or' (('not' b) 'or' ('not' a))) by BVFUNC_1:8
.= ('not' a) 'or' ((b 'or' ('not' b)) 'or' ('not' a)) by BVFUNC_1:8
.= ('not' a) 'or' ((I_el Y) 'or' ('not' a)) by BVFUNC_4:6
.= ('not' a) 'or' (I_el Y) by BVFUNC_1:10 ;
hence  (a 'imp' b) 'or' (a 'imp' ('not' b)) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:28
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y
('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = ('not' ('not' a)) 'or' (('not' b) 'eqv' (b 'imp' a)) by BVFUNC_4:8
.= a 'or' ((('not' b) 'imp' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:7
.= a 'or' ((('not' ('not' b)) 'or' (b 'imp' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:8
.= a 'or' ((b 'or' (('not' b) 'or' a)) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:8
.= a 'or' (((b 'or' ('not' b)) 'or' a) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_1:8
.= a 'or' (((I_el Y) 'or' a) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_4:6
.= a 'or' ((I_el Y) '&' ((b 'imp' a) 'imp' ('not' b))) by BVFUNC_1:10
.= a 'or' ((b 'imp' a) 'imp' ('not' b)) by BVFUNC_1:6
.= a 'or' ((('not' b) 'or' a) 'imp' ('not' b)) by BVFUNC_4:8
.= a 'or' (('not' (('not' b) 'or' a)) 'or' ('not' b)) by BVFUNC_4:8
.= a 'or' ((('not' ('not' b)) '&' ('not' a)) 'or' ('not' b)) by BVFUNC_1:13
.= a 'or' ((b 'or' ('not' b)) '&' (('not' a) 'or' ('not' b))) by BVFUNC_1:11
.= a 'or' ((I_el Y) '&' (('not' a) 'or' ('not' b))) by BVFUNC_4:6
.= a 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:6
.= (a 'or' ('not' a)) 'or' ('not' b) by BVFUNC_1:8
.= (I_el Y) 'or' ('not' b) by BVFUNC_4:6 ;
hence  ('not' a) 'imp' (('not' b) 'eqv' (b 'imp' a)) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y
(a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = ('not' (a 'imp' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' b)) 'or' (((a 'imp' c) 'imp' b) 'imp' b) by BVFUNC_1:13
.= (a '&' ('not' b)) 'or' (('not' ((a 'imp' c) 'imp' b)) 'or' b) by BVFUNC_4:8
.= (a '&' ('not' b)) 'or' (('not' ((('not' a) 'or' c) 'imp' b)) 'or' b) by BVFUNC_4:8
.= (a '&' ('not' b)) 'or' (('not' (('not' (('not' a) 'or' c)) 'or' b)) 'or' b) by BVFUNC_4:8
.= (a '&' ('not' b)) 'or' (('not' ((('not' ('not' a)) '&' ('not' c)) 'or' b)) 'or' b) by BVFUNC_1:13
.= (a '&' ('not' b)) 'or' ((('not' (a '&' ('not' c))) '&' ('not' b)) 'or' b) by BVFUNC_1:13
.= (a '&' ('not' b)) 'or' (((('not' a) 'or' ('not' ('not' c))) '&' ('not' b)) 'or' b) by BVFUNC_1:14
.= (a '&' ('not' b)) 'or' (((('not' a) 'or' c) 'or' b) '&' (('not' b) 'or' b)) by BVFUNC_1:11
.= (a '&' ('not' b)) 'or' (((('not' a) 'or' c) 'or' b) '&' (I_el Y)) by BVFUNC_4:6
.= (a '&' ('not' b)) 'or' ((('not' a) 'or' c) 'or' b) by BVFUNC_1:6
.= ((a '&' ('not' b)) 'or' b) 'or' (('not' a) 'or' c) by BVFUNC_1:8
.= ((a 'or' b) '&' (('not' b) 'or' b)) 'or' (('not' a) 'or' c) by BVFUNC_1:11
.= ((a 'or' b) '&' (I_el Y)) 'or' (('not' a) 'or' c) by BVFUNC_4:6
.= (a 'or' b) 'or' (('not' a) 'or' c) by BVFUNC_1:6
.= b 'or' (a 'or' (('not' a) 'or' c)) by BVFUNC_1:8
.= b 'or' ((a 'or' ('not' a)) 'or' c) by BVFUNC_1:8
.= b 'or' ((I_el Y) 'or' c) by BVFUNC_4:6
.= b 'or' (I_el Y) by BVFUNC_1:10 ;
hence  (a 'imp' b) 'imp' (((a 'imp' c) 'imp' b) 'imp' b) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:30
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = a 'eqv' (a '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = a 'eqv' (a '&' b)
a 'eqv' (a '&' b) = (a 'imp' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:7
.= (('not' a) 'or' (a '&' b)) '&' ((a '&' b) 'imp' a) by BVFUNC_4:8
.= (('not' a) 'or' (a '&' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_4:8
.= ((('not' a) 'or' a) '&' (('not' a) 'or' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_1:11
.= ((I_el Y) '&' (('not' a) 'or' b)) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_4:6
.= (('not' a) 'or' b) '&' (('not' (a '&' b)) 'or' a) by BVFUNC_1:6
.= (('not' a) 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' a) by BVFUNC_1:14
.= (('not' a) 'or' b) '&' (('not' b) 'or' (('not' a) 'or' a)) by BVFUNC_1:8
.= (('not' a) 'or' b) '&' (('not' b) 'or' (I_el Y)) by BVFUNC_4:6
.= (('not' a) 'or' b) '&' (I_el Y) by BVFUNC_1:10
.= ('not' a) 'or' b by BVFUNC_1:6 ;
hence  a 'imp' b = a 'eqv' (a '&' b) by BVFUNC_4:8; ::_thesis: verum
end;

theorem :: BVFUNC25:31
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds
( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )
let a, b be Function of Y,BOOLEAN; ::_thesis: ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b )
 ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) by BVFUNC_4:10;
hence  ( ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) iff a = b ) by BVFUNC_1:17; ::_thesis: verum
end;

theorem :: BVFUNC25:32
for Y being non empty set
for a being Function of Y,BOOLEAN holds a = ('not' a) 'imp' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a = ('not' a) 'imp' a
let a be Function of Y,BOOLEAN; ::_thesis: a = ('not' a) 'imp' a
 (('not' a) 'imp' a) 'imp' a = I_el Y by BVFUNC_5:11;
then A1: ('not' a) 'imp' a '<' a by BVFUNC_1:16;
 a 'imp' (('not' a) 'imp' a) = I_el Y by Th22;
then  a '<' ('not' a) 'imp' a by BVFUNC_1:16;
hence  a = ('not' a) 'imp' a by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem Th33: :: BVFUNC25:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' ((a 'imp' b) 'imp' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' ((a 'imp' b) 'imp' a) = I_el Y
thus a 'imp' ((a 'imp' b) 'imp' a) = ('not' a) 'or' ((a 'imp' b) 'imp' a) by BVFUNC_4:8
.= ('not' a) 'or' (('not' (a 'imp' b)) 'or' a) by BVFUNC_4:8
.= ('not' a) 'or' (('not' (('not' a) 'or' b)) 'or' a) by BVFUNC_4:8
.= ('not' a) 'or' ((('not' ('not' a)) '&' ('not' b)) 'or' a) by BVFUNC_1:13
.= (('not' a) 'or' a) 'or' (a '&' ('not' b)) by BVFUNC_1:8
.= (I_el Y) 'or' (a '&' ('not' b)) by BVFUNC_4:6
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

theorem :: BVFUNC25:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a = (a 'imp' b) 'imp' a
 ((a 'imp' b) 'imp' a) 'imp' a = I_el Y by BVFUNC_8:27;
then A1: (a 'imp' b) 'imp' a '<' a by BVFUNC_1:16;
 a 'imp' ((a 'imp' b) 'imp' a) = I_el Y by Th33;
then  a '<' (a 'imp' b) 'imp' a by BVFUNC_1:16;
hence  a = (a 'imp' b) 'imp' a by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC25:35
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (b 'imp' a) '&' (('not' b) 'imp' a)
let a, b be Function of Y,BOOLEAN; ::_thesis: a = (b 'imp' a) '&' (('not' b) 'imp' a)
a = (a 'or' b) '&' (a 'or' ('not' b)) by BVFUNC_8:7
.= (a 'or' ('not' ('not' b))) '&' (b 'imp' a) by BVFUNC_4:8
.= (('not' b) 'imp' a) '&' (b 'imp' a) by BVFUNC_4:8 ;
hence  a = (b 'imp' a) '&' (('not' b) 'imp' a) ; ::_thesis: verum
end;

theorem :: BVFUNC25:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b = 'not' (a 'imp' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b = 'not' (a 'imp' ('not' b))
 ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y by BVFUNC_6:35;
then A1: 'not' (a 'imp' ('not' b)) '<' a '&' b by BVFUNC_1:16;
 (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y by BVFUNC_6:34;
then  a '&' b '<' 'not' (a 'imp' ('not' b)) by BVFUNC_1:16;
hence  a '&' b = 'not' (a 'imp' ('not' b)) by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC25:37
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' b = ('not' a) 'imp' b
thus ('not' a) 'imp' b = ('not' ('not' a)) 'or' b by BVFUNC_4:8
.= a 'or' b ; ::_thesis: verum
end;

theorem :: BVFUNC25:38
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = (a 'imp' b) 'imp' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' b = (a 'imp' b) 'imp' b
thus (a 'imp' b) 'imp' b = ('not' (a 'imp' b)) 'or' b by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' b by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' b)) 'or' b by BVFUNC_1:13
.= (a 'or' b) '&' (('not' b) 'or' b) by BVFUNC_1:11
.= (a 'or' b) '&' (I_el Y) by BVFUNC_4:6
.= a 'or' b by BVFUNC_1:6 ; ::_thesis: verum
end;

theorem :: BVFUNC25:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (a 'imp' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (a 'imp' a) = I_el Y
thus (a 'imp' b) 'imp' (a 'imp' a) = (a 'imp' b) 'imp' (I_el Y) by BVFUNC_5:7
.= I_el Y by BVFUNC_7:16 ; ::_thesis: verum
end;

theorem :: BVFUNC25:40
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = I_el Y
thus (a 'imp' (b 'imp' c)) 'imp' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) = ('not' (a 'imp' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (b 'imp' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' ((d 'imp' b) 'imp' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (d 'imp' b)) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (a 'imp' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (d 'imp' c))) by BVFUNC_4:8
.= ('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' (('not' b) 'or' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13
.= (('not' ('not' a)) '&' (('not' ('not' b)) '&' ('not' c))) 'or' (('not' (('not' d) 'or' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13
.= (a '&' (('not' ('not' b)) '&' ('not' c))) 'or' ((('not' ('not' d)) '&' ('not' b)) 'or' (('not' a) 'or' (('not' d) 'or' c))) by BVFUNC_1:13
.= (a '&' (b '&' ('not' c))) 'or' (((d '&' ('not' b)) 'or' ('not' a)) 'or' (('not' d) 'or' c)) by BVFUNC_1:8
.= ((a '&' (b '&' ('not' c))) 'or' (('not' a) 'or' (d '&' ('not' b)))) 'or' (('not' d) 'or' c) by BVFUNC_1:8
.= (((a '&' (b '&' ('not' c))) 'or' ('not' a)) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:8
.= (((a 'or' ('not' a)) '&' ((b '&' ('not' c)) 'or' ('not' a))) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:11
.= (((I_el Y) '&' ((b '&' ('not' c)) 'or' ('not' a))) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_4:6
.= (((b '&' ('not' c)) 'or' ('not' a)) 'or' (d '&' ('not' b))) 'or' (('not' d) 'or' c) by BVFUNC_1:6
.= ((b '&' ('not' c)) 'or' ('not' a)) 'or' ((d '&' ('not' b)) 'or' (('not' d) 'or' c)) by BVFUNC_1:8
.= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) '&' d) 'or' ('not' d)) 'or' c) by BVFUNC_1:8
.= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) 'or' ('not' d)) '&' (d 'or' ('not' d))) 'or' c) by BVFUNC_1:11
.= ((b '&' ('not' c)) 'or' ('not' a)) 'or' (((('not' b) 'or' ('not' d)) '&' (I_el Y)) 'or' c) by BVFUNC_4:6
.= ((b '&' ('not' c)) 'or' ('not' a)) 'or' ((('not' b) 'or' ('not' d)) 'or' c) by BVFUNC_1:6
.= ('not' a) 'or' ((('not' c) '&' b) 'or' ((('not' b) 'or' ('not' d)) 'or' c)) by BVFUNC_1:8
.= ('not' a) 'or' (((('not' c) '&' b) 'or' (('not' b) 'or' ('not' d))) 'or' c) by BVFUNC_1:8
.= ('not' a) 'or' ((((('not' c) '&' b) 'or' ('not' b)) 'or' ('not' d)) 'or' c) by BVFUNC_1:8
.= ('not' a) 'or' ((((('not' c) 'or' ('not' b)) '&' (b 'or' ('not' b))) 'or' ('not' d)) 'or' c) by BVFUNC_1:11
.= ('not' a) 'or' ((((('not' c) 'or' ('not' b)) '&' (I_el Y)) 'or' ('not' d)) 'or' c) by BVFUNC_4:6
.= ('not' a) 'or' (((('not' b) 'or' ('not' c)) 'or' ('not' d)) 'or' c) by BVFUNC_1:6
.= ('not' a) 'or' ((('not' b) 'or' (('not' c) 'or' ('not' d))) 'or' c) by BVFUNC_1:8
.= ('not' a) 'or' (('not' b) 'or' ((('not' d) 'or' ('not' c)) 'or' c)) by BVFUNC_1:8
.= ('not' a) 'or' (('not' b) 'or' (('not' d) 'or' (('not' c) 'or' c))) by BVFUNC_1:8
.= ('not' a) 'or' (('not' b) 'or' (('not' d) 'or' (I_el Y))) by BVFUNC_4:6
.= ('not' a) 'or' (('not' b) 'or' (I_el Y)) by BVFUNC_1:10
.= ('not' a) 'or' (I_el Y) by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

theorem :: BVFUNC25:41
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'imp' b) '&' a) '&' c) 'imp' b = I_el Y
thus (((a 'imp' b) '&' a) '&' c) 'imp' b = (((('not' a) 'or' b) '&' a) '&' c) 'imp' b by BVFUNC_4:8
.= (((('not' a) '&' a) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_1:12
.= (((O_el Y) 'or' (b '&' a)) '&' c) 'imp' b by BVFUNC_4:5
.= ((b '&' a) '&' c) 'imp' b by BVFUNC_1:9
.= ('not' ((b '&' a) '&' c)) 'or' b by BVFUNC_4:8
.= (('not' (b '&' a)) 'or' ('not' c)) 'or' b by BVFUNC_1:14
.= ((('not' b) 'or' ('not' a)) 'or' ('not' c)) 'or' b by BVFUNC_1:14
.= (b 'or' (('not' b) 'or' ('not' a))) 'or' ('not' c) by BVFUNC_1:8
.= ((b 'or' ('not' b)) 'or' ('not' a)) 'or' ('not' c) by BVFUNC_1:8
.= ((I_el Y) 'or' ('not' a)) 'or' ('not' c) by BVFUNC_4:6
.= (I_el Y) 'or' ('not' c) by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

theorem :: BVFUNC25:42
for Y being non empty set
for b, c, a being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for b, c, a being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y
let b, c, a be Function of Y,BOOLEAN; ::_thesis: (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = I_el Y
thus (b 'imp' c) 'imp' ((a '&' b) 'imp' c) = ('not' (b 'imp' c)) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8
.= ('not' (('not' b) 'or' c)) 'or' ((a '&' b) 'imp' c) by BVFUNC_4:8
.= ('not' (('not' b) 'or' c)) 'or' (('not' (a '&' b)) 'or' c) by BVFUNC_4:8
.= (('not' ('not' b)) '&' ('not' c)) 'or' (('not' (a '&' b)) 'or' c) by BVFUNC_1:13
.= (b '&' ('not' c)) 'or' ((('not' a) 'or' ('not' b)) 'or' c) by BVFUNC_1:14
.= ((b '&' ('not' c)) 'or' c) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:8
.= ((b 'or' c) '&' (('not' c) 'or' c)) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:11
.= ((b 'or' c) '&' (I_el Y)) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:6
.= (('not' a) 'or' ('not' b)) 'or' (b 'or' c) by BVFUNC_1:6
.= ((('not' a) 'or' ('not' b)) 'or' b) 'or' c by BVFUNC_1:8
.= (('not' a) 'or' (('not' b) 'or' b)) 'or' c by BVFUNC_1:8
.= (('not' a) 'or' (I_el Y)) 'or' c by BVFUNC_4:6
.= (I_el Y) 'or' c by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ; ::_thesis: verum
end;

theorem :: BVFUNC25:43
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y
((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = (('not' (a '&' b)) 'or' c) 'imp' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8
.= ('not' (('not' (a '&' b)) 'or' c)) 'or' ((a '&' b) 'imp' (c '&' b)) by BVFUNC_4:8
.= ('not' (('not' (a '&' b)) 'or' c)) 'or' (('not' (a '&' b)) 'or' (c '&' b)) by BVFUNC_4:8
.= (('not' ('not' (a '&' b))) '&' ('not' c)) 'or' (('not' (a '&' b)) 'or' (c '&' b)) by BVFUNC_1:13
.= ((a '&' b) '&' ('not' c)) 'or' ((('not' a) 'or' ('not' b)) 'or' (c '&' b)) by BVFUNC_1:14
.= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' (('not' b) 'or' (b '&' c))) by BVFUNC_1:8
.= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' ((('not' b) 'or' b) '&' (('not' b) 'or' c))) by BVFUNC_1:11
.= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' ((I_el Y) '&' (('not' b) 'or' c))) by BVFUNC_4:6
.= ((a '&' b) '&' ('not' c)) 'or' (('not' a) 'or' (('not' b) 'or' c)) by BVFUNC_1:6
.= (((a '&' b) '&' ('not' c)) 'or' ('not' a)) 'or' (('not' b) 'or' c) by BVFUNC_1:8
.= (((a '&' b) 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:11
.= (((a 'or' ('not' a)) '&' (b 'or' ('not' a))) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:11
.= (((I_el Y) '&' (b 'or' ('not' a))) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_4:6
.= ((b 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' (('not' b) 'or' c) by BVFUNC_1:6
.= (((b 'or' ('not' a)) '&' (('not' c) 'or' ('not' a))) 'or' c) 'or' ('not' b) by BVFUNC_1:8
.= (((b 'or' ('not' a)) 'or' c) '&' ((('not' c) 'or' ('not' a)) 'or' c)) 'or' ('not' b) by BVFUNC_1:11
.= (((b 'or' ('not' a)) 'or' c) '&' (('not' a) 'or' (('not' c) 'or' c))) 'or' ('not' b) by BVFUNC_1:8
.= (((b 'or' ('not' a)) 'or' c) '&' (('not' a) 'or' (I_el Y))) 'or' ('not' b) by BVFUNC_4:6
.= (((b 'or' ('not' a)) 'or' c) '&' (I_el Y)) 'or' ('not' b) by BVFUNC_1:10
.= ((b 'or' ('not' a)) 'or' c) 'or' ('not' b) by BVFUNC_1:6
.= (('not' b) 'or' (b 'or' ('not' a))) 'or' c by BVFUNC_1:8
.= ((('not' b) 'or' b) 'or' ('not' a)) 'or' c by BVFUNC_1:8
.= ((I_el Y) 'or' ('not' a)) 'or' c by BVFUNC_4:6
.= (I_el Y) 'or' c by BVFUNC_1:10 ;
hence  ((a '&' b) 'imp' c) 'imp' ((a '&' b) 'imp' (c '&' b)) = I_el Y by BVFUNC_1:10; ::_thesis: verum
end;

theorem :: BVFUNC25:44
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y
 a 'imp' b '<' (a '&' c) 'imp' (b '&' c) by BVFUNC_9:10;
hence  (a 'imp' b) 'imp' ((a '&' c) 'imp' (b '&' c)) = I_el Y by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC25:45
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y
((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = (((a 'imp' b) '&' a) '&' c) 'imp' (b '&' c) by BVFUNC_1:4
.= ((a '&' b) '&' c) 'imp' (b '&' c) by BVFUNC_7:10
.= (a '&' (b '&' c)) 'imp' (b '&' c) by BVFUNC_1:4 ;
hence  ((a 'imp' b) '&' (a '&' c)) 'imp' (b '&' c) = I_el Y by BVFUNC_6:38; ::_thesis: verum
end;

theorem :: BVFUNC25:46
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c
((a '&' (a 'imp' b)) '&' (b 'imp' c)) 'imp' c = ('not' ((a '&' (a 'imp' b)) '&' (b 'imp' c))) 'or' c by BVFUNC_4:8
.= ('not' ((a '&' b) '&' (b 'imp' c))) 'or' c by BVFUNC_7:10
.= ('not' (a '&' (b '&' (b 'imp' c)))) 'or' c by BVFUNC_1:4
.= ('not' (a '&' (b '&' c))) 'or' c by BVFUNC_7:10
.= ('not' ((a '&' b) '&' c)) 'or' c by BVFUNC_1:4
.= (('not' (a '&' b)) 'or' ('not' c)) 'or' c by BVFUNC_1:14
.= ('not' (a '&' b)) 'or' (('not' c) 'or' c) by BVFUNC_1:8
.= ('not' (a '&' b)) 'or' (I_el Y) by BVFUNC_4:6
.= I_el Y by BVFUNC_1:10 ;
hence  (a '&' (a 'imp' b)) '&' (b 'imp' c) '<' c by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC25:47
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c)
(((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c)) 'imp' (('not' a) 'imp' (b 'or' c)) = ('not' (((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8
.= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (b 'imp' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8
.= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c))) 'or' (('not' a) 'imp' (b 'or' c)) by BVFUNC_4:8
.= ('not' (((a 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_4:8
.= (('not' ((a 'or' b) '&' (('not' a) 'or' c))) 'or' ('not' (('not' b) 'or' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:14
.= (('not' ((a 'or' b) '&' (('not' a) 'or' c))) 'or' (('not' ('not' b)) '&' ('not' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:13
.= ((('not' (a 'or' b)) 'or' ('not' (('not' a) 'or' c))) 'or' (b '&' ('not' c))) 'or' (('not' ('not' a)) 'or' (b 'or' c)) by BVFUNC_1:14
.= (((('not' a) '&' ('not' b)) 'or' ('not' (('not' a) 'or' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13
.= (((('not' a) '&' ('not' b)) 'or' (('not' ('not' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:13
.= (((('not' a) 'or' (a '&' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11
.= ((((('not' a) 'or' a) '&' (('not' a) 'or' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:11
.= ((((I_el Y) '&' (('not' a) 'or' ('not' c))) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:6
.= (((('not' a) 'or' ('not' c)) '&' (('not' b) 'or' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:6
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((('not' a) 'or' ('not' c)) '&' (a '&' ('not' c)))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((('not' a) 'or' ('not' c)) '&' a) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:4
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((('not' a) '&' a) 'or' (('not' c) '&' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:12
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((O_el Y) 'or' (('not' c) '&' a)) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_4:5
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((('not' c) '&' a) '&' ('not' c))) 'or' (b '&' ('not' c))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:9
.= (((('not' c) '&' a) '&' ('not' c)) 'or' (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c)))) 'or' (a 'or' (b 'or' c)) by BVFUNC_1:8
.= (((('not' c) '&' a) '&' ('not' c)) 'or' (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c)))) 'or' (c 'or' (a 'or' b)) by BVFUNC_1:8
.= (((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) '&' a) '&' ('not' c))) 'or' c) 'or' (a 'or' b) by BVFUNC_1:8
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) '&' ('not' c)) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:8
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) 'or' c) '&' (('not' c) 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (((('not' c) '&' a) 'or' c) '&' (I_el Y))) 'or' (a 'or' b) by BVFUNC_4:6
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) '&' a) 'or' c)) 'or' (a 'or' b) by BVFUNC_1:6
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((('not' c) 'or' c) '&' (a 'or' c))) 'or' (a 'or' b) by BVFUNC_1:11
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' ((I_el Y) '&' (a 'or' c))) 'or' (a 'or' b) by BVFUNC_4:6
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (a 'or' c)) 'or' (a 'or' b) by BVFUNC_1:6
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((b '&' ('not' c)) 'or' (c 'or' a))) 'or' (a 'or' b) by BVFUNC_1:8
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b '&' ('not' c)) 'or' c) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:8
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b 'or' c) '&' (('not' c) 'or' c)) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (((b 'or' c) '&' (I_el Y)) 'or' a)) 'or' (a 'or' b) by BVFUNC_4:6
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' ((b 'or' c) 'or' a)) 'or' (a 'or' b) by BVFUNC_1:6
.= (((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' (b 'or' (c 'or' a))) 'or' (a 'or' b) by BVFUNC_1:8
.= ((((('not' a) 'or' ('not' c)) '&' ('not' b)) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:8
.= ((((('not' a) 'or' ('not' c)) 'or' b) '&' (('not' b) 'or' b)) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:11
.= ((((('not' a) 'or' ('not' c)) 'or' b) '&' (I_el Y)) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_4:6
.= (((('not' a) 'or' ('not' c)) 'or' b) 'or' (c 'or' a)) 'or' (a 'or' b) by BVFUNC_1:6
.= ((((('not' a) 'or' ('not' c)) 'or' b) 'or' c) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8
.= ((((('not' a) 'or' ('not' c)) 'or' c) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8
.= (((('not' a) 'or' (('not' c) 'or' c)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:8
.= (((('not' a) 'or' (I_el Y)) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_4:6
.= (((I_el Y) 'or' b) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10
.= ((I_el Y) 'or' a) 'or' (a 'or' b) by BVFUNC_1:10
.= (I_el Y) 'or' (a 'or' b) by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ;
hence  ((a 'or' b) '&' (a 'imp' c)) '&' (b 'imp' c) '<' ('not' a) 'imp' (b 'or' c) by BVFUNC_1:16; ::_thesis: verum
end;