let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
let a, b, c be Function of Y,BOOLEAN; :: thesis: ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
set K1 = (a 'imp' c) '&' (b 'imp' c);
(a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c by Th20;
then A1: ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' ((a 'or' b) 'imp' c) '&' (a 'or' b) by Th33;
((a 'or' b) 'imp' c) '&' (a 'or' b) '<' c by Th2;
hence ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c by A1, BVFUNC_1:15; :: thesis: verum