let Y be 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)
let a, b, c be Function of Y,BOOLEAN; ((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; verum