let Y be non empty set ; for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)
let x be Element of Y; FUNCT_2:def 8 K11((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)),x) = K11((((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)),x)
((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) =
((('not' a) 'or' b) '&' (b 'imp' c)) '&' (c 'imp' a)
by BVFUNC_4:8
.=
((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (c 'imp' a)
by BVFUNC_4:8
.=
((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)
by BVFUNC_4:8
.=
((('not' a) '&' (('not' b) 'or' c)) 'or' (b '&' (('not' b) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:12
.=
((('not' a) '&' (('not' b) 'or' c)) 'or' ((b '&' ('not' b)) 'or' (b '&' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:12
.=
((('not' a) '&' (('not' b) 'or' c)) 'or' ((O_el Y) 'or' (b '&' c))) '&' (('not' c) 'or' a)
by BVFUNC_4:5
.=
((('not' a) '&' (('not' b) 'or' c)) 'or' (b '&' c)) '&' (('not' c) 'or' a)
by BVFUNC_1:9
.=
((('not' a) 'or' (b '&' c)) '&' ((('not' b) 'or' c) 'or' (b '&' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:11
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) 'or' c) 'or' (b '&' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:11
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (((('not' b) 'or' c) 'or' b) '&' ((('not' b) 'or' c) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:11
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((c 'or' (('not' b) 'or' b)) '&' ((('not' b) 'or' c) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:8
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((c 'or' (I_el Y)) '&' ((('not' b) 'or' c) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_4:6
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((I_el Y) '&' ((('not' b) 'or' c) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:10
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) 'or' c) 'or' c)) '&' (('not' c) 'or' a)
by BVFUNC_1:6
.=
(((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' (c 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:8
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) 'or' c) '&' (('not' c) 'or' a))
by BVFUNC_1:4
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) '&' (('not' c) 'or' a)) 'or' (c '&' (('not' c) 'or' a)))
by BVFUNC_1:12
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) '&' (('not' c) 'or' a)) 'or' ((c '&' ('not' c)) 'or' (c '&' a)))
by BVFUNC_1:12
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) '&' (('not' c) 'or' a)) 'or' ((O_el Y) 'or' (c '&' a)))
by BVFUNC_4:5
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) '&' (('not' c) 'or' a)) 'or' (c '&' a))
by BVFUNC_1:9
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' ((('not' b) 'or' (c '&' a)) '&' ((('not' c) 'or' a) 'or' (c '&' a)))
by BVFUNC_1:11
.=
((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (((('not' b) 'or' c) '&' (('not' b) 'or' a)) '&' ((('not' c) 'or' a) 'or' (c '&' a)))
by BVFUNC_1:11
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) 'or' c) '&' ((('not' c) 'or' a) 'or' a)))
by BVFUNC_1:11
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' ((a 'or' (('not' c) 'or' c)) '&' ((('not' c) 'or' a) 'or' a)))
by BVFUNC_1:8
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' ((a 'or' (I_el Y)) '&' ((('not' c) 'or' a) 'or' a)))
by BVFUNC_4:6
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' ((I_el Y) '&' ((('not' c) 'or' a) 'or' a)))
by BVFUNC_1:10
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' ((('not' c) 'or' a) 'or' a))
by BVFUNC_1:6
.=
((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' (((('not' b) 'or' a) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' (a 'or' a)))
by BVFUNC_1:8
.=
(((('not' a) 'or' c) '&' (('not' a) 'or' b)) '&' ((('not' b) 'or' a) '&' (('not' b) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:4
.=
((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' a)) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)
by BVFUNC_1:4
.=
((((('not' b) 'or' a) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' b)) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)
by BVFUNC_1:4
.=
(((('not' b) 'or' a) '&' (('not' a) 'or' c)) '&' ((('not' a) 'or' b) '&' (('not' b) 'or' c))) '&' (('not' c) 'or' a)
by BVFUNC_1:4
.=
((('not' b) 'or' a) '&' (('not' a) 'or' c)) '&' (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a))
by BVFUNC_1:4
.=
((('not' b) 'or' a) '&' (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a))) '&' (('not' a) 'or' c)
by BVFUNC_1:4
.=
((((a 'imp' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)) '&' (('not' b) 'or' a)) '&' (('not' a) 'or' c)
by BVFUNC_4:8
.=
((((a 'imp' b) '&' (b 'imp' c)) '&' (('not' c) 'or' a)) '&' (('not' b) 'or' a)) '&' (('not' a) 'or' c)
by BVFUNC_4:8
.=
((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (('not' b) 'or' a)) '&' (('not' a) 'or' c)
by BVFUNC_4:8
.=
((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (('not' a) 'or' c)
by BVFUNC_4:8
.=
((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)
by BVFUNC_4:8
;
hence
K11((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)),x) = K11((((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)),x)
; verum