let Y be non empty set ; :: thesis: for a, b, c, d being Element of Funcs (Y,BOOLEAN) st a '<' b & c '<' d holds
a '&' c '<' b '&' d
let a, b, c, d be Element of Funcs (Y,BOOLEAN); :: thesis: ( a '<' b & c '<' d implies a '&' c '<' b '&' d )
assume ( a '<' b & c '<' d ) ; :: thesis: a '&' c '<' b '&' d
then ( a 'imp' b = I_el Y & c 'imp' d = I_el Y ) by BVFUNC_1:16;
then (a '&' c) 'imp' (b '&' d) = I_el Y by BVFUNC_6:21;
hence a '&' c '<' b '&' d by BVFUNC_1:16; :: thesis: verum