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