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 )
A1: (((d '&' c) '&' b) '&' a) 'imp' a = I_el Y by BVFUNC_6:39;
((a '&' b) '&' c) '&' d = (d '&' c) '&' (b '&' a) by BVFUNC_1:7
.= ((d '&' c) '&' b) '&' a by BVFUNC_1:7 ;
hence ((a '&' b) '&' c) '&' d '<' a by A1, BVFUNC_1:19; :: thesis: ((a '&' b) '&' c) '&' d '<' b
A2: (((a '&' c) '&' d) '&' b) 'imp' b = I_el Y by BVFUNC_6:39;
((a '&' b) '&' c) '&' d = ((a '&' c) '&' b) '&' d by BVFUNC_1:7
.= ((a '&' c) '&' d) '&' b by BVFUNC_1:7 ;
hence ((a '&' b) '&' c) '&' d '<' b by A2, BVFUNC_1:19; :: thesis: verum