let Y be non empty set ; :: thesis: for a, c, b being Element of Funcs (Y,BOOLEAN) holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
let a, c, b be Element of Funcs (Y,BOOLEAN); :: thesis: ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
(a 'imp' c) 'or' (b 'imp' c) = (a '&' b) 'imp' c by BVFUNC_7:6;
hence ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c by Th2; :: thesis: verum