let Y be non empty set ; for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )
let a, b, c, d, e be Function of Y,BOOLEAN; ( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )
A1:
((((e '&' d) '&' c) '&' b) '&' a) 'imp' a = I_el Y
by Th38;
(((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; (((a '&' b) '&' c) '&' d) '&' e '<' b
A2:
((((a '&' c) '&' d) '&' e) '&' b) 'imp' b = I_el Y
by Th38;
(((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; verum