let Y be non empty set ; :: thesis: for a, c, b being Element of Funcs Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
let a, c, b be Element of Funcs 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 Th21;
then A1: ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' ((a 'or' b) 'imp' c) '&' (a 'or' b) by Th34;
((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:18; :: thesis: verum