let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '&' ('not' c) '<' 'not' b
let a, b, c be Function of Y,BOOLEAN; :: thesis: ( a '&' b '<' c implies a '&' ('not' c) '<' 'not' b )
assume a '&' b '<' c ; :: thesis: a '&' ('not' c) '<' 'not' b
then I_el Y = (a '&' b) 'imp' c by BVFUNC_1:16
.= ('not' (a '&' b)) 'or' c by BVFUNC_4:8
.= (('not' a) 'or' ('not' b)) 'or' c by BVFUNC_1:14
.= (('not' a) 'or' ('not' ('not' c))) 'or' ('not' b) by BVFUNC_1:8
.= ('not' (a '&' ('not' c))) 'or' ('not' b) by BVFUNC_1:14
.= (a '&' ('not' c)) 'imp' ('not' b) by BVFUNC_4:8 ;
hence a '&' ('not' c) '<' 'not' b by BVFUNC_1:16; :: thesis: verum