let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )
let a, b, c be Element of Funcs Y,BOOLEAN ; :: thesis: ( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )
A1: (a '&' b) '&' c = (c '&' b) '&' a by BVFUNC_1:7;
((c '&' b) '&' a) 'imp' a = I_el Y by BVFUNC_6:39;
hence (a '&' b) '&' c '<' a by A1, BVFUNC_1:19; :: thesis: (a '&' b) '&' c '<' b
A2: (a '&' b) '&' c = (a '&' c) '&' b by BVFUNC_1:7;
((a '&' c) '&' b) 'imp' b = I_el Y by BVFUNC_6:39;
hence (a '&' b) '&' c '<' b by A2, BVFUNC_1:19; :: thesis: verum