let Y be non empty set ; for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y
let a, b, c be Function of Y,BOOLEAN; (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y
let x be Element of Y; FUNCT_2:def 8 ((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x = (I_el Y) . x
A1: ((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x =
('not' ((a 'imp' b) . x)) 'or' ((('not' (b '&' c)) 'imp' ('not' (a '&' c))) . x)
by BVFUNC_1:def 8
.=
('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x))
by BVFUNC_1:def 8
;
A2: ('not' (a '&' c)) . x =
(('not' a) 'or' ('not' c)) . x
by BVFUNC_1:14
.=
(('not' a) . x) 'or' (('not' c) . x)
by BVFUNC_1:def 4
.=
('not' (a . x)) 'or' (('not' c) . x)
by MARGREL1:def 19
.=
('not' (a . x)) 'or' ('not' (c . x))
by MARGREL1:def 19
;
then
('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x)) = TRUE
by BINARITH:10;
then A3:
((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' (('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x))) = (('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)
by MARGREL1:14;
'not' (('not' (b '&' c)) . x) =
'not' ('not' ((b '&' c) . x))
by MARGREL1:def 19
.=
(b . x) '&' (c . x)
by MARGREL1:def 20
;
then A6: ('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x) =
((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (c . x))
by A2, XBOOLEAN:9
.=
((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' (('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x)))
by BINARITH:11
;
'not' ((a 'imp' b) . x) =
'not' (('not' (a . x)) 'or' (b . x))
by BVFUNC_1:def 8
.=
(a . x) '&' ('not' (b . x))
;
then ('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x)) =
(((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' (((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' ('not' (b . x)))
by A6, A3, XBOOLEAN:9
.=
(((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x))))
by BINARITH:11
.=
(((('not' (c . x)) 'or' ('not' (a . x))) 'or' (a . x)) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x))))
by BINARITH:11
.=
((('not' (c . x)) 'or' (('not' (a . x)) 'or' (a . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x))))
by BINARITH:11
;
then ('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x)) =
(TRUE 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' TRUE)
by A4, A5, BINARITH:10
.=
TRUE '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' TRUE)
by BINARITH:10
.=
TRUE '&' TRUE
by BINARITH:10
.=
TRUE
;
hence
((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x = (I_el Y) . x
by A1, BVFUNC_1:def 11; verum