let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: ( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
A1: (((d '&' c) '&' b) '&' a) 'imp' a = I_el Y by Th38;
((a '&' b) '&' c) '&' d = (d '&' c) '&' (b '&' a) by BVFUNC_1:4
.= ((d '&' c) '&' b) '&' a by BVFUNC_1:4 ;
hence ((a '&' b) '&' c) '&' d '<' a by A1, BVFUNC_1:16; :: thesis: ((a '&' b) '&' c) '&' d '<' b
A2: (((a '&' c) '&' d) '&' b) 'imp' b = I_el Y by Th38;
((a '&' b) '&' c) '&' d = ((a '&' c) '&' b) '&' d by BVFUNC_1:4
.= ((a '&' c) '&' d) '&' b by BVFUNC_1:4 ;
hence ((a '&' b) '&' c) '&' d '<' b by A2, BVFUNC_1:16; :: thesis: verum