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