let Y be non empty set ; :: thesis: for a, b, c, d, e, f, g being Element of Funcs Y,BOOLEAN holds
( ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' a = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' b = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' c = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' d = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' e = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' f = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' g = I_el Y )
let a, b, c, d, e, f, g be Element of Funcs Y,BOOLEAN ; :: thesis: ( ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' a = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' b = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' c = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' d = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' e = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' f = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' g = I_el Y )
A1: ( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) by Lm6;
A2: (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' g by Lm1;
A3: ( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' e & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' f ) by Lm2, Lm3;
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' c & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' d ) by Lm4, Lm5;
hence ( ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' a = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' b = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' c = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' d = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' e = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' f = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' g = I_el Y ) by A1, A3, A2, BVFUNC_1:19; :: thesis: verum