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

proof

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

end;

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