let Y be non empty set ; :: thesis: for a, b, c, d being Element of Funcs Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
let a, b, c, d be Element of Funcs Y,BOOLEAN ; :: thesis: ( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
thus ((a '&' b) '&' c) '&' d '<' a :: thesis: ((a '&' b) '&' c) '&' d '<' b

proof

A1: ((a '&' b) '&' c) '&' d = (d '&' c) '&' (b '&' a) by BVFUNC_1:7
.= ((d '&' c) '&' b) '&' a by BVFUNC_1:7 ;
(((d '&' c) '&' b) '&' a) 'imp' a = I_el Y by BVFUNC_6:39;
hence ((a '&' b) '&' c) '&' d '<' a by A1, BVFUNC_1:19; :: thesis: verum

end;

A2: ((a '&' b) '&' c) '&' d = ((a '&' c) '&' b) '&' d by BVFUNC_1:7
.= ((a '&' c) '&' d) '&' b by BVFUNC_1:7 ;
(((a '&' c) '&' d) '&' b) 'imp' b = I_el Y by BVFUNC_6:39;
hence ((a '&' b) '&' c) '&' d '<' b by A2, BVFUNC_1:19; :: thesis: verum