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