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