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