:: BVFUNC_8 semantic presentation

begin

theorem :: BVFUNC_8:1
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' ((b '&' c) '&' d)) . x = (((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)) . x
(((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)) . x = (((a 'imp' b) '&' (a 'imp' c)) . x) '&' ((a 'imp' d) . x) by MARGREL1:def_20
.= (((a 'imp' b) . x) '&' ((a 'imp' c) . x)) '&' ((a 'imp' d) . x) by MARGREL1:def_20
.= ((('not' (a . x)) 'or' (b . x)) '&' ((a 'imp' c) . x)) '&' ((a 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' (c . x))) '&' ((a 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' (c . x))) '&' (('not' (a . x)) 'or' (d . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ((b . x) '&' (c . x))) '&' (('not' (a . x)) 'or' (d . x)) by XBOOLEAN:9
.= ('not' (a . x)) 'or' (((b . x) '&' (c . x)) '&' (d . x)) by XBOOLEAN:9
.= ('not' (a . x)) 'or' (((b '&' c) . x) '&' (d . x)) by MARGREL1:def_20
.= ('not' (a . x)) 'or' (((b '&' c) '&' d) . x) by MARGREL1:def_20
.= (a 'imp' ((b '&' c) '&' d)) . x by BVFUNC_1:def_8 ;
hence  (a 'imp' ((b '&' c) '&' d)) . x = (((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:2
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' ((b 'or' c) 'or' d)) . x = (((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)) . x
(((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)) . x = (((a 'imp' b) 'or' (a 'imp' c)) . x) 'or' ((a 'imp' d) . x) by BVFUNC_1:def_4
.= (((a 'imp' b) . x) 'or' ((a 'imp' c) . x)) 'or' ((a 'imp' d) . x) by BVFUNC_1:def_4
.= ((('not' (a . x)) 'or' (b . x)) 'or' ((a 'imp' c) . x)) 'or' ((a 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) 'or' (('not' (a . x)) 'or' (c . x))) 'or' ((a 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (b . x)) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (d . x)) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (('not' (a . x)) 'or' (b . x))) 'or' (c . x)) 'or' (('not' (a . x)) 'or' (d . x)) by BINARITH:11
.= (((('not' (a . x)) 'or' ('not' (a . x))) 'or' (b . x)) 'or' (c . x)) 'or' (('not' (a . x)) 'or' (d . x)) by BINARITH:11
.= (('not' (a . x)) 'or' ((b . x) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (d . x)) by BINARITH:11
.= (('not' (a . x)) 'or' ((b 'or' c) . x)) 'or' (('not' (a . x)) 'or' (d . x)) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (('not' (a . x)) 'or' ((b 'or' c) . x))) 'or' (d . x) by BINARITH:11
.= ((('not' (a . x)) 'or' ('not' (a . x))) 'or' ((b 'or' c) . x)) 'or' (d . x) by BINARITH:11
.= ('not' (a . x)) 'or' (((b 'or' c) . x) 'or' (d . x)) by BINARITH:11
.= ('not' (a . x)) 'or' (((b 'or' c) 'or' d) . x) by BVFUNC_1:def_4
.= (a 'imp' ((b 'or' c) 'or' d)) . x by BVFUNC_1:def_8 ;
hence  (a 'imp' ((b 'or' c) 'or' d)) . x = (((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:3
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (((a '&' b) '&' c) 'imp' d) . x = (((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)) . x
(((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)) . x = (((a 'imp' d) 'or' (b 'imp' d)) . x) 'or' ((c 'imp' d) . x) by BVFUNC_1:def_4
.= (((a 'imp' d) . x) 'or' ((b 'imp' d) . x)) 'or' ((c 'imp' d) . x) by BVFUNC_1:def_4
.= ((('not' (a . x)) 'or' (d . x)) 'or' ((b 'imp' d) . x)) 'or' ((c 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (d . x)) 'or' (('not' (b . x)) 'or' (d . x))) 'or' ((c 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (d . x)) 'or' (('not' (b . x)) 'or' (d . x))) 'or' (('not' (c . x)) 'or' (d . x)) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' ((d . x) 'or' ('not' (b . x)))) 'or' (d . x)) 'or' (('not' (c . x)) 'or' (d . x)) by BINARITH:11
.= (((('not' (a . x)) 'or' ('not' (b . x))) 'or' (d . x)) 'or' (d . x)) 'or' (('not' (c . x)) 'or' (d . x)) by BINARITH:11
.= ((('not' (a . x)) 'or' ('not' (b . x))) 'or' ((d . x) 'or' (d . x))) 'or' (('not' (c . x)) 'or' (d . x)) by BINARITH:11
.= (('not' ((a . x) '&' (b . x))) 'or' ((d . x) 'or' ('not' (c . x)))) 'or' (d . x) by BINARITH:11
.= ((('not' ((a . x) '&' (b . x))) 'or' ('not' (c . x))) 'or' (d . x)) 'or' (d . x) by BINARITH:11
.= (('not' ((a . x) '&' (b . x))) 'or' ('not' (c . x))) 'or' ((d . x) 'or' (d . x)) by BINARITH:11
.= ('not' (((a '&' b) . x) '&' (c . x))) 'or' (d . x) by MARGREL1:def_20
.= ('not' (((a '&' b) '&' c) . x)) 'or' (d . x) by MARGREL1:def_20
.= (((a '&' b) '&' c) 'imp' d) . x by BVFUNC_1:def_8 ;
hence  (((a '&' b) '&' c) 'imp' d) . x = (((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:4
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (((a 'or' b) 'or' c) 'imp' d) . x = (((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)) . x
(((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)) . x = (((a 'imp' d) '&' (b 'imp' d)) . x) '&' ((c 'imp' d) . x) by MARGREL1:def_20
.= (((a 'imp' d) . x) '&' ((b 'imp' d) . x)) '&' ((c 'imp' d) . x) by MARGREL1:def_20
.= ((('not' (a . x)) 'or' (d . x)) '&' ((b 'imp' d) . x)) '&' ((c 'imp' d) . x) by BVFUNC_1:def_8
.= ((('not' (a . x)) 'or' (d . x)) '&' (('not' (b . x)) 'or' (d . x))) '&' ((c 'imp' d) . x) by BVFUNC_1:def_8
.= (((d . x) 'or' ('not' (a . x))) '&' (('not' (b . x)) 'or' (d . x))) '&' (('not' (c . x)) 'or' (d . x)) by BVFUNC_1:def_8
.= (('not' ((a . x) 'or' (b . x))) 'or' (d . x)) '&' (('not' (c . x)) 'or' (d . x)) by XBOOLEAN:9
.= ((d . x) 'or' ('not' ((a 'or' b) . x))) '&' (('not' (c . x)) 'or' (d . x)) by BVFUNC_1:def_4
.= ('not' (((a 'or' b) . x) 'or' (c . x))) 'or' (d . x) by XBOOLEAN:9
.= ('not' (((a 'or' b) 'or' c) . x)) 'or' (d . x) by BVFUNC_1:def_4
.= (((a 'or' b) 'or' c) 'imp' d) . x by BVFUNC_1:def_8 ;
hence  (((a 'or' b) 'or' c) 'imp' d) . x = (((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:5
for Y being 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)
proof
let Y be non empty set ; ::_thesis: 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; ::_thesis: ((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; :: according to FUNCT_2:def_8 ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . x = (((((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  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . x = (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:6
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a = (a '&' b) 'or' (a '&' ('not' b))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = ((a '&' b) 'or' (a '&' ('not' b))) . x
((a '&' b) 'or' (a '&' ('not' b))) . x = (a '&' (b 'or' ('not' b))) . x by BVFUNC_1:12
.= (a '&' (I_el Y)) . x by BVFUNC_4:6
.= a . x by BVFUNC_1:6 ;
hence  a . x = ((a '&' b) 'or' (a '&' ('not' b))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:7
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'or' b) '&' (a 'or' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a = (a 'or' b) '&' (a 'or' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a = (a 'or' b) '&' (a 'or' ('not' b))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = ((a 'or' b) '&' (a 'or' ('not' b))) . x
((a 'or' b) '&' (a 'or' ('not' b))) . x = (a 'or' (b '&' ('not' b))) . x by BVFUNC_1:11
.= (a 'or' (O_el Y)) . x by BVFUNC_4:5
.= a . x by BVFUNC_1:9 ;
hence  a . x = ((a 'or' b) '&' (a 'or' ('not' b))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = (((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x
(((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x = ((((a '&' b) '&' (c 'or' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x by BVFUNC_1:12
.= ((((a '&' b) '&' (I_el Y)) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x by BVFUNC_4:6
.= (((a '&' b) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x by BVFUNC_1:6
.= ((a '&' b) 'or' (((a '&' ('not' b)) '&' c) 'or' ((a '&' ('not' b)) '&' ('not' c)))) . x by BVFUNC_1:8
.= ((a '&' b) 'or' ((a '&' ('not' b)) '&' (c 'or' ('not' c)))) . x by BVFUNC_1:12
.= ((a '&' b) 'or' ((a '&' ('not' b)) '&' (I_el Y))) . x by BVFUNC_4:6
.= ((a '&' b) 'or' (a '&' ('not' b))) . x by BVFUNC_1:6
.= (a '&' (b 'or' ('not' b))) . x by BVFUNC_1:12
.= (a '&' (I_el Y)) . x by BVFUNC_4:6
.= a . x by BVFUNC_1:6 ;
hence  a . x = (((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a = ((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a = ((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: a . x = (((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x
(((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x = ((((a 'or' b) 'or' (c '&' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x by BVFUNC_1:11
.= ((((a 'or' b) 'or' (O_el Y)) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x by BVFUNC_4:5
.= (((a 'or' b) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x by BVFUNC_1:9
.= ((a 'or' b) '&' (((a 'or' ('not' b)) 'or' c) '&' ((a 'or' ('not' b)) 'or' ('not' c)))) . x by BVFUNC_1:4
.= ((a 'or' b) '&' ((a 'or' ('not' b)) 'or' (c '&' ('not' c)))) . x by BVFUNC_1:11
.= ((a 'or' b) '&' ((a 'or' ('not' b)) 'or' (O_el Y))) . x by BVFUNC_4:5
.= ((a 'or' b) '&' (a 'or' ('not' b))) . x by BVFUNC_1:9
.= (a 'or' (b '&' ('not' b))) . x by BVFUNC_1:11
.= (a 'or' (O_el Y)) . x by BVFUNC_4:5
.= a . x by BVFUNC_1:9 ;
hence  a . x = (((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = a '&' (('not' a) 'or' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b = a '&' (('not' a) 'or' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b = a '&' (('not' a) 'or' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' b) . x = (a '&' (('not' a) 'or' b)) . x
(a '&' (('not' a) 'or' b)) . x = (a . x) '&' ((('not' a) 'or' b) . x) by MARGREL1:def_20
.= (a . x) '&' ((('not' a) . x) 'or' (b . x)) by BVFUNC_1:def_4
.= ((a . x) '&' (('not' a) . x)) 'or' ((a . x) '&' (b . x)) by XBOOLEAN:8
.= ((a . x) '&' ('not' (a . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19
.= FALSE 'or' ((a . x) '&' (b . x)) by XBOOLEAN:138
.= (a . x) '&' (b . x) by BINARITH:3
.= (a '&' b) . x by MARGREL1:def_20 ;
hence  (a '&' b) . x = (a '&' (('not' a) 'or' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = a 'or' (('not' a) '&' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = a 'or' (('not' a) '&' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' b = a 'or' (('not' a) '&' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' b) . x = (a 'or' (('not' a) '&' b)) . x
(a 'or' (('not' a) '&' b)) . x = (a . x) 'or' ((('not' a) '&' b) . x) by BVFUNC_1:def_4
.= (a . x) 'or' ((('not' a) . x) '&' (b . x)) by MARGREL1:def_20
.= ((a . x) 'or' (('not' a) . x)) '&' ((a . x) 'or' (b . x)) by XBOOLEAN:9
.= ((a . x) 'or' ('not' (a . x))) '&' ((a . x) 'or' (b . x)) by MARGREL1:def_19
.= TRUE '&' ((a . x) 'or' (b . x)) by XBOOLEAN:102
.= (a . x) 'or' (b . x) by MARGREL1:14
.= (a 'or' b) . x by BVFUNC_1:def_4 ;
hence  (a 'or' b) . x = (a 'or' (('not' a) '&' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:12
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = 'not' (a 'eqv' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' b = 'not' (a 'eqv' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' b = 'not' (a 'eqv' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' b) . x = ('not' (a 'eqv' b)) . x
(a 'xor' b) . x = ('not' ('not' ((('not' a) '&' b) 'or' (a '&' ('not' b))))) . x by BVFUNC_4:9
.= ('not' (('not' (('not' a) '&' b)) '&' ('not' (a '&' ('not' b))))) . x by BVFUNC_1:13
.= ('not' ((('not' ('not' a)) 'or' ('not' b)) '&' ('not' (a '&' ('not' b))))) . x by BVFUNC_1:14
.= ('not' ((a 'or' ('not' b)) '&' (('not' a) 'or' ('not' ('not' b))))) . x by BVFUNC_1:14
.= ('not' ((b 'imp' a) '&' (('not' a) 'or' b))) . x by BVFUNC_4:8
.= ('not' ((b 'imp' a) '&' (a 'imp' b))) . x by BVFUNC_4:8
.= ('not' (a 'eqv' b)) . x by BVFUNC_4:7 ;
hence  (a 'xor' b) . x = ('not' (a 'eqv' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:13
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (a 'or' b) '&' (('not' a) 'or' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' b = (a 'or' b) '&' (('not' a) 'or' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' b = (a 'or' b) '&' (('not' a) 'or' ('not' b))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' b) . x = ((a 'or' b) '&' (('not' a) 'or' ('not' b))) . x
((a 'or' b) '&' (('not' a) 'or' ('not' b))) . x = ((a 'or' b) . x) '&' ((('not' a) 'or' ('not' b)) . x) by MARGREL1:def_20
.= ((a . x) 'or' (b . x)) '&' ((('not' a) 'or' ('not' b)) . x) by BVFUNC_1:def_4
.= ((a . x) 'or' (b . x)) '&' ((('not' a) . x) 'or' (('not' b) . x)) by BVFUNC_1:def_4
.= ((('not' a) . x) '&' ((a . x) 'or' (b . x))) 'or' (((a . x) 'or' (b . x)) '&' (('not' b) . x)) by XBOOLEAN:8
.= (((('not' a) . x) '&' (a . x)) 'or' ((('not' a) . x) '&' (b . x))) 'or' ((('not' b) . x) '&' ((a . x) 'or' (b . x))) by XBOOLEAN:8
.= (((('not' a) . x) '&' (a . x)) 'or' ((('not' a) . x) '&' (b . x))) 'or' (((('not' b) . x) '&' (a . x)) 'or' ((('not' b) . x) '&' (b . x))) by XBOOLEAN:8
.= ((('not' (a . x)) '&' (a . x)) 'or' ((('not' a) . x) '&' (b . x))) 'or' (((('not' b) . x) '&' (a . x)) 'or' ((('not' b) . x) '&' (b . x))) by MARGREL1:def_19
.= ((('not' (a . x)) '&' (a . x)) 'or' ((('not' a) . x) '&' (b . x))) 'or' (((('not' b) . x) '&' (a . x)) 'or' (('not' (b . x)) '&' (b . x))) by MARGREL1:def_19
.= (FALSE 'or' ((('not' a) . x) '&' (b . x))) 'or' (((('not' b) . x) '&' (a . x)) 'or' (('not' (b . x)) '&' (b . x))) by XBOOLEAN:138
.= (FALSE 'or' ((('not' a) . x) '&' (b . x))) 'or' (((('not' b) . x) '&' (a . x)) 'or' FALSE) by XBOOLEAN:138
.= ((('not' a) . x) '&' (b . x)) 'or' (((('not' b) . x) '&' (a . x)) 'or' FALSE) by BINARITH:3
.= ((('not' a) . x) '&' (b . x)) 'or' ((a . x) '&' (('not' b) . x)) by BINARITH:3
.= ((('not' a) '&' b) . x) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_20
.= ((('not' a) '&' b) . x) 'or' ((a '&' ('not' b)) . x) by MARGREL1:def_20
.= ((('not' a) '&' b) 'or' (a '&' ('not' b))) . x by BVFUNC_1:def_4
.= (a 'xor' b) . x by BVFUNC_4:9 ;
hence  (a 'xor' b) . x = ((a 'or' b) '&' (('not' a) 'or' ('not' b))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:14
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (I_el Y) = 'not' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' (I_el Y) = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' (I_el Y) = 'not' a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' (I_el Y)) . x = ('not' a) . x
(a 'xor' (I_el Y)) . x = ((('not' a) '&' (I_el Y)) 'or' (a '&' ('not' (I_el Y)))) . x by BVFUNC_4:9
.= ((('not' a) '&' (I_el Y)) 'or' (a '&' (O_el Y))) . x by BVFUNC_1:2
.= ((('not' a) '&' (I_el Y)) 'or' (O_el Y)) . x by BVFUNC_1:5
.= (('not' a) '&' (I_el Y)) . x by BVFUNC_1:9
.= ('not' a) . x by BVFUNC_1:6 ;
hence  (a 'xor' (I_el Y)) . x = ('not' a) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:15
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (O_el Y) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'xor' (O_el Y) = a
let a be Function of Y,BOOLEAN; ::_thesis: a 'xor' (O_el Y) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' (O_el Y)) . x = a . x
(a 'xor' (O_el Y)) . x = ((('not' a) '&' (O_el Y)) 'or' (a '&' ('not' (O_el Y)))) . x by BVFUNC_4:9
.= ((('not' a) '&' (O_el Y)) 'or' (a '&' (I_el Y))) . x by BVFUNC_1:2
.= ((('not' a) '&' (O_el Y)) 'or' a) . x by BVFUNC_1:6
.= ((O_el Y) 'or' a) . x by BVFUNC_1:5
.= a . x by BVFUNC_1:9 ;
hence  (a 'xor' (O_el Y)) . x = a . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:16
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = ('not' a) 'xor' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' b = ('not' a) 'xor' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' b = ('not' a) 'xor' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' b) . x = (('not' a) 'xor' ('not' b)) . x
(('not' a) 'xor' ('not' b)) . x = ((('not' ('not' a)) '&' ('not' b)) 'or' (('not' a) '&' ('not' ('not' b)))) . x by BVFUNC_4:9
.= (a 'xor' b) . x by BVFUNC_4:9 ;
hence  (a 'xor' b) . x = (('not' a) 'xor' ('not' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:17
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'xor' b) = a 'xor' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (a 'xor' b)) . x = (a 'xor' ('not' b)) . x
('not' (a 'xor' b)) . x = ('not' ((('not' a) '&' b) 'or' (a '&' ('not' b)))) . x by BVFUNC_4:9
.= (('not' (('not' a) '&' b)) '&' ('not' (a '&' ('not' b)))) . x by BVFUNC_1:13
.= ((('not' ('not' a)) 'or' ('not' b)) '&' ('not' (a '&' ('not' b)))) . x by BVFUNC_1:14
.= ((a 'or' ('not' b)) '&' (('not' a) 'or' ('not' ('not' b)))) . x by BVFUNC_1:14
.= (((a 'or' ('not' b)) '&' ('not' a)) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:12
.= (((a '&' ('not' a)) 'or' (('not' b) '&' ('not' a))) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:12
.= (((O_el Y) 'or' (('not' b) '&' ('not' a))) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_4:5
.= ((('not' b) '&' ('not' a)) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:9
.= ((('not' b) '&' ('not' a)) 'or' ((a '&' b) 'or' (('not' b) '&' b))) . x by BVFUNC_1:12
.= ((('not' b) '&' ('not' a)) 'or' ((a '&' b) 'or' (O_el Y))) . x by BVFUNC_4:5
.= ((('not' a) '&' ('not' b)) 'or' (a '&' ('not' ('not' b)))) . x by BVFUNC_1:9
.= (a 'xor' ('not' b)) . x by BVFUNC_4:9 ;
hence  ('not' (a 'xor' b)) . x = (a 'xor' ('not' b)) . x ; ::_thesis: verum
end;

theorem Th18: :: BVFUNC_8:18
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' ('not' b)) '&' (('not' a) 'or' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' ('not' b)) '&' (('not' a) 'or' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a 'or' ('not' b)) '&' (('not' a) 'or' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' b) . x = ((a 'or' ('not' b)) '&' (('not' a) 'or' b)) . x
((a 'or' ('not' b)) '&' (('not' a) 'or' b)) . x = ((a 'or' ('not' b)) '&' (a 'imp' b)) . x by BVFUNC_4:8
.= ((a 'imp' b) '&' (b 'imp' a)) . x by BVFUNC_4:8
.= (a 'eqv' b) . x by BVFUNC_4:7 ;
hence  (a 'eqv' b) . x = ((a 'or' ('not' b)) '&' (('not' a) 'or' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:19
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a '&' b) 'or' (('not' a) '&' ('not' b))
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a '&' b) 'or' (('not' a) '&' ('not' b))
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a '&' b) 'or' (('not' a) '&' ('not' b))
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' b) . x = ((a '&' b) 'or' (('not' a) '&' ('not' b))) . x
((a '&' b) 'or' (('not' a) '&' ('not' b))) . x = (((a '&' b) 'or' ('not' a)) '&' ((a '&' b) 'or' ('not' b))) . x by BVFUNC_1:11
.= (((a 'or' ('not' a)) '&' (b 'or' ('not' a))) '&' ((a '&' b) 'or' ('not' b))) . x by BVFUNC_1:11
.= (((a 'or' ('not' a)) '&' (b 'or' ('not' a))) '&' ((a 'or' ('not' b)) '&' (b 'or' ('not' b)))) . x by BVFUNC_1:11
.= (((I_el Y) '&' (b 'or' ('not' a))) '&' ((a 'or' ('not' b)) '&' (b 'or' ('not' b)))) . x by BVFUNC_4:6
.= (((I_el Y) '&' (b 'or' ('not' a))) '&' ((a 'or' ('not' b)) '&' (I_el Y))) . x by BVFUNC_4:6
.= ((b 'or' ('not' a)) '&' ((a 'or' ('not' b)) '&' (I_el Y))) . x by BVFUNC_1:6
.= ((b 'or' ('not' a)) '&' (a 'or' ('not' b))) . x by BVFUNC_1:6
.= (a 'eqv' b) . x by Th18 ;
hence  (a 'eqv' b) . x = ((a '&' b) 'or' (('not' a) '&' ('not' b))) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:20
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a
let a be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (I_el Y) = a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' (I_el Y)) . x = a . x
(a 'eqv' (I_el Y)) . x = ((a 'imp' (I_el Y)) '&' ((I_el Y) 'imp' a)) . x by BVFUNC_4:7
.= ((('not' a) 'or' (I_el Y)) '&' ((I_el Y) 'imp' a)) . x by BVFUNC_4:8
.= ((('not' a) 'or' (I_el Y)) '&' (('not' (I_el Y)) 'or' a)) . x by BVFUNC_4:8
.= ((I_el Y) '&' (('not' (I_el Y)) 'or' a)) . x by BVFUNC_1:10
.= ((I_el Y) '&' ((O_el Y) 'or' a)) . x by BVFUNC_1:2
.= ((I_el Y) '&' a) . x by BVFUNC_1:9
.= a . x by BVFUNC_1:6 ;
hence  (a 'eqv' (I_el Y)) . x = a . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:21
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (O_el Y) = 'not' a
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'eqv' (O_el Y) = 'not' a
let a be Function of Y,BOOLEAN; ::_thesis: a 'eqv' (O_el Y) = 'not' a
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' (O_el Y)) . x = ('not' a) . x
(a 'eqv' (O_el Y)) . x = ((a 'imp' (O_el Y)) '&' ((O_el Y) 'imp' a)) . x by BVFUNC_4:7
.= ((('not' a) 'or' (O_el Y)) '&' ((O_el Y) 'imp' a)) . x by BVFUNC_4:8
.= ((('not' a) 'or' (O_el Y)) '&' (('not' (O_el Y)) 'or' a)) . x by BVFUNC_4:8
.= (('not' a) '&' (('not' (O_el Y)) 'or' a)) . x by BVFUNC_1:9
.= (('not' a) '&' ((I_el Y) 'or' a)) . x by BVFUNC_1:2
.= (('not' a) '&' (I_el Y)) . x by BVFUNC_1:10
.= ('not' a) . x by BVFUNC_1:6 ;
hence  (a 'eqv' (O_el Y)) . x = ('not' a) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:22
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' (a 'eqv' b) = a 'eqv' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (a 'eqv' b)) . x = (a 'eqv' ('not' b)) . x
('not' (a 'eqv' b)) . x = ('not' ((a 'imp' b) '&' (b 'imp' a))) . x by BVFUNC_4:7
.= ('not' ((('not' a) 'or' b) '&' (b 'imp' a))) . x by BVFUNC_4:8
.= ('not' ((('not' a) 'or' b) '&' (('not' b) 'or' a))) . x by BVFUNC_4:8
.= (('not' (('not' a) 'or' b)) 'or' ('not' (('not' b) 'or' a))) . x by BVFUNC_1:14
.= ((('not' ('not' a)) '&' ('not' b)) 'or' ('not' (('not' b) 'or' a))) . x by BVFUNC_1:13
.= ((a '&' ('not' b)) 'or' (('not' ('not' b)) '&' ('not' a))) . x by BVFUNC_1:13
.= (((a '&' ('not' b)) 'or' b) '&' ((a '&' ('not' b)) 'or' ('not' a))) . x by BVFUNC_1:11
.= (((a 'or' b) '&' (('not' b) 'or' b)) '&' ((a '&' ('not' b)) 'or' ('not' a))) . x by BVFUNC_1:11
.= (((a 'or' b) '&' (('not' b) 'or' b)) '&' ((a 'or' ('not' a)) '&' (('not' b) 'or' ('not' a)))) . x by BVFUNC_1:11
.= (((a 'or' b) '&' (I_el Y)) '&' ((a 'or' ('not' a)) '&' (('not' b) 'or' ('not' a)))) . x by BVFUNC_4:6
.= (((a 'or' b) '&' (I_el Y)) '&' ((I_el Y) '&' (('not' b) 'or' ('not' a)))) . x by BVFUNC_4:6
.= ((a 'or' b) '&' ((I_el Y) '&' (('not' b) 'or' ('not' a)))) . x by BVFUNC_1:6
.= ((('not' a) 'or' ('not' b)) '&' (('not' ('not' b)) 'or' a)) . x by BVFUNC_1:6
.= ((('not' a) 'or' ('not' b)) '&' (('not' b) 'imp' a)) . x by BVFUNC_4:8
.= ((a 'imp' ('not' b)) '&' (('not' b) 'imp' a)) . x by BVFUNC_4:8
.= (a 'eqv' ('not' b)) . x by BVFUNC_4:7 ;
hence  ('not' (a 'eqv' b)) . x = (a 'eqv' ('not' b)) . x ; ::_thesis: verum
end;

theorem :: BVFUNC_8:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (a 'imp' b) 'eqv' ('not' a)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' a '<' (a 'imp' b) 'eqv' ('not' a)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' a '<' (a 'imp' b) 'eqv' ('not' a)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' a) . z = TRUE or ((a 'imp' b) 'eqv' ('not' a)) . z = TRUE )
assume A1: ('not' a) . z = TRUE ; ::_thesis: ((a 'imp' b) 'eqv' ('not' a)) . z = TRUE
then  'not' (a . z) = TRUE by MARGREL1:def_19;
then A2: a . z = FALSE by MARGREL1:11;
((a 'imp' b) 'eqv' ('not' a)) . z = ((('not' a) 'or' b) 'eqv' ('not' a)) . z by BVFUNC_4:8
.= (((('not' a) 'or' b) 'imp' ('not' a)) '&' (('not' a) 'imp' (('not' a) 'or' b))) . z by BVFUNC_4:7
.= ((('not' (('not' a) 'or' b)) 'or' ('not' a)) '&' (('not' a) 'imp' (('not' a) 'or' b))) . z by BVFUNC_4:8
.= ((('not' (('not' a) 'or' b)) 'or' ('not' a)) '&' (('not' ('not' a)) 'or' (('not' a) 'or' b))) . z by BVFUNC_4:8
.= ((('not' (('not' a) 'or' b)) 'or' ('not' a)) . z) '&' ((('not' ('not' a)) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_20
.= ((('not' (('not' a) 'or' b)) . z) 'or' (('not' a) . z)) '&' ((('not' ('not' a)) 'or' (('not' a) 'or' b)) . z) by BVFUNC_1:def_4
.= (('not' ((('not' a) 'or' b) . z)) 'or' (('not' a) . z)) '&' ((('not' ('not' a)) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_19
.= (('not' ((('not' a) . z) 'or' (b . z))) 'or' (('not' a) . z)) '&' ((('not' ('not' a)) 'or' (('not' a) 'or' b)) . z) by BVFUNC_1:def_4
.= ((('not' ('not' (a . z))) '&' ('not' (b . z))) 'or' (('not' a) . z)) '&' ((('not' ('not' a)) 'or' (('not' a) 'or' b)) . z) by MARGREL1:def_19
.= (((a . z) '&' ('not' (b . z))) 'or' (('not' a) . z)) '&' ((('not' ('not' a)) . z) 'or' ((('not' a) 'or' b) . z)) by BVFUNC_1:def_4
.= (((a . z) '&' ('not' (b . z))) 'or' (('not' a) . z)) '&' ((a . z) 'or' ((('not' a) . z) 'or' (b . z))) by BVFUNC_1:def_4
.= TRUE '&' (FALSE 'or' (TRUE 'or' (b . z))) by A1, A2, BINARITH:10
.= FALSE 'or' (TRUE 'or' (b . z)) by MARGREL1:14
.= TRUE 'or' (b . z) by BINARITH:3
.= TRUE by BINARITH:10 ;
hence  ((a 'imp' b) 'eqv' ('not' a)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_8:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (b 'imp' a) 'eqv' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds 'not' a '<' (b 'imp' a) 'eqv' ('not' b)
let a, b be Function of Y,BOOLEAN; ::_thesis: 'not' a '<' (b 'imp' a) 'eqv' ('not' b)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' a) . z = TRUE or ((b 'imp' a) 'eqv' ('not' b)) . z = TRUE )
assume  ('not' a) . z = TRUE ; ::_thesis: ((b 'imp' a) 'eqv' ('not' b)) . z = TRUE
then A1: 'not' (a . z) = TRUE by MARGREL1:def_19;
((b 'imp' a) 'eqv' ('not' b)) . z = ((('not' b) 'or' a) 'eqv' ('not' b)) . z by BVFUNC_4:8
.= (((('not' b) 'or' a) 'imp' ('not' b)) '&' (('not' b) 'imp' (('not' b) 'or' a))) . z by BVFUNC_4:7
.= ((('not' (('not' b) 'or' a)) 'or' ('not' b)) '&' (('not' b) 'imp' (('not' b) 'or' a))) . z by BVFUNC_4:8
.= ((('not' (('not' b) 'or' a)) 'or' ('not' b)) '&' (('not' ('not' b)) 'or' (('not' b) 'or' a))) . z by BVFUNC_4:8
.= ((('not' (('not' b) 'or' a)) 'or' ('not' b)) . z) '&' ((('not' ('not' b)) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_20
.= ((('not' (('not' b) 'or' a)) . z) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) 'or' (('not' b) 'or' a)) . z) by BVFUNC_1:def_4
.= (('not' ((('not' b) 'or' a) . z)) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_19
.= (('not' ((('not' b) . z) 'or' (a . z))) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) 'or' (('not' b) 'or' a)) . z) by BVFUNC_1:def_4
.= ((('not' ('not' (b . z))) '&' ('not' (a . z))) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) 'or' (('not' b) 'or' a)) . z) by MARGREL1:def_19
.= (((b . z) '&' ('not' (a . z))) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) . z) 'or' ((('not' b) 'or' a) . z)) by BVFUNC_1:def_4
.= (((b . z) '&' ('not' (a . z))) 'or' (('not' b) . z)) '&' ((('not' ('not' b)) . z) 'or' ((('not' b) . z) 'or' (a . z))) by BVFUNC_1:def_4
.= (((b . z) '&' ('not' (a . z))) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' (b . z)) 'or' (a . z))) by MARGREL1:def_19
.= ((TRUE '&' (b . z)) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' (b . z)) 'or' FALSE)) by A1, MARGREL1:11
.= ((b . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' (b . z)) 'or' FALSE)) by MARGREL1:14
.= ((b . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' (('not' (b . z)) 'or' FALSE)) by MARGREL1:def_19
.= TRUE '&' ((b . z) 'or' (('not' (b . z)) 'or' FALSE)) by XBOOLEAN:102
.= (b . z) 'or' (('not' (b . z)) 'or' FALSE) by MARGREL1:14
.= ((b . z) 'or' ('not' (b . z))) 'or' FALSE by BINARITH:11
.= TRUE 'or' FALSE by XBOOLEAN:102
.= TRUE by BINARITH:10 ;
hence  ((b 'imp' a) 'eqv' ('not' b)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_8:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not a . z = TRUE or (((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a) . z = TRUE )
assume A1: a . z = TRUE ; ::_thesis: (((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a) . z = TRUE
A2: ((a 'or' b) 'eqv' (b 'or' a)) . z = (((a 'or' b) 'imp' (a 'or' b)) '&' ((a 'or' b) 'imp' (a 'or' b))) . z by BVFUNC_4:7
.= (('not' (a 'or' b)) 'or' (a 'or' b)) . z by BVFUNC_4:8
.= (I_el Y) . z by BVFUNC_4:6
.= TRUE by BVFUNC_1:def_11 ;
(((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a) . z = ((((a 'or' b) 'eqv' (a 'or' b)) 'imp' a) '&' (a 'imp' ((a 'or' b) 'eqv' (a 'or' b)))) . z by BVFUNC_4:7
.= ((((a 'or' b) 'eqv' (a 'or' b)) 'imp' a) . z) '&' ((a 'imp' ((a 'or' b) 'eqv' (a 'or' b))) . z) by MARGREL1:def_20
.= ((('not' ((a 'or' b) 'eqv' (a 'or' b))) 'or' a) . z) '&' ((a 'imp' ((a 'or' b) 'eqv' (a 'or' b))) . z) by BVFUNC_4:8
.= ((('not' ((a 'or' b) 'eqv' (a 'or' b))) 'or' a) . z) '&' ((('not' a) 'or' ((a 'or' b) 'eqv' (a 'or' b))) . z) by BVFUNC_4:8
.= ((('not' ((a 'or' b) 'eqv' (a 'or' b))) . z) 'or' (a . z)) '&' ((('not' a) 'or' ((a 'or' b) 'eqv' (a 'or' b))) . z) by BVFUNC_1:def_4
.= ((('not' ((a 'or' b) 'eqv' (a 'or' b))) . z) 'or' (a . z)) '&' ((('not' a) . z) 'or' (((a 'or' b) 'eqv' (a 'or' b)) . z)) by BVFUNC_1:def_4
.= (('not' (((a 'or' b) 'eqv' (a 'or' b)) . z)) 'or' (a . z)) '&' ((('not' a) . z) 'or' (((a 'or' b) 'eqv' (a 'or' b)) . z)) by MARGREL1:def_19
.= (FALSE 'or' (a . z)) '&' ((('not' a) . z) 'or' TRUE) by A2, MARGREL1:11
.= (a . z) '&' ((('not' a) . z) 'or' TRUE) by BINARITH:3
.= (a . z) '&' TRUE by BINARITH:10
.= TRUE by A1 ;
hence  (((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_8:26
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y
 for x being Element of Y holds (a 'imp' (('not' a) 'eqv' ('not' a))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (('not' a) 'eqv' ('not' a))) . x = TRUE
(a 'imp' (('not' a) 'eqv' ('not' a))) . x = (('not' a) 'or' (('not' a) 'eqv' ('not' a))) . x by BVFUNC_4:8
.= (('not' a) 'or' ((('not' a) 'imp' ('not' a)) '&' (('not' a) 'imp' ('not' a)))) . x by BVFUNC_4:7
.= (('not' a) 'or' (('not' ('not' a)) 'or' ('not' a))) . x by BVFUNC_4:8
.= (('not' a) 'or' (I_el Y)) . x by BVFUNC_4:6
.= TRUE by BVFUNC_1:def_11, BVFUNC_1:10 ;
hence  (a 'imp' (('not' a) 'eqv' ('not' a))) . x = TRUE ; ::_thesis: verum
end;
hence  a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_8:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' a) 'imp' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' a) 'imp' a = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) 'imp' a) 'imp' a = I_el Y
 for x being Element of Y holds (((a 'imp' b) 'imp' a) 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'imp' b) 'imp' a) 'imp' a) . x = TRUE
(((a 'imp' b) 'imp' a) 'imp' a) . x = (('not' ((a 'imp' b) 'imp' a)) 'or' a) . x by BVFUNC_4:8
.= (('not' (('not' (a 'imp' b)) 'or' a)) 'or' a) . x by BVFUNC_4:8
.= (('not' (('not' (('not' a) 'or' b)) 'or' a)) 'or' a) . x by BVFUNC_4:8
.= (('not' ((('not' ('not' a)) '&' ('not' b)) 'or' a)) 'or' a) . x by BVFUNC_1:13
.= (('not' ((a 'or' a) '&' (('not' b) 'or' a))) 'or' a) . x by BVFUNC_1:11
.= ((('not' a) 'or' ('not' (('not' b) 'or' a))) 'or' a) . x by BVFUNC_1:14
.= ((('not' a) 'or' (('not' ('not' b)) '&' ('not' a))) 'or' a) . x by BVFUNC_1:13
.= (((('not' a) 'or' b) '&' (('not' a) 'or' ('not' a))) 'or' a) . x by BVFUNC_1:11
.= (((('not' a) 'or' b) 'or' a) '&' (('not' a) 'or' a)) . x by BVFUNC_1:11
.= (((('not' a) 'or' b) 'or' a) '&' (I_el Y)) . x by BVFUNC_4:6
.= ((('not' a) 'or' b) 'or' a) . x by BVFUNC_1:6
.= (b 'or' (('not' a) 'or' a)) . x by BVFUNC_1:8
.= (b 'or' (I_el Y)) . x by BVFUNC_4:6
.= TRUE by BVFUNC_1:def_11, BVFUNC_1:10 ;
hence  (((a 'imp' b) 'imp' a) 'imp' a) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'imp' b) 'imp' a) 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_8:28
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
 for x being Element of Y holds ((((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE
(((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = ('not' (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:8
.= ('not' (((('not' a) 'or' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:8
.= ('not' (((('not' a) 'or' c) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:8
.= (('not' ((('not' a) 'or' c) '&' (('not' b) 'or' d))) 'or' ('not' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:14
.= ((('not' (('not' a) 'or' c)) 'or' ('not' (('not' b) 'or' d))) 'or' ('not' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:14
.= (((('not' ('not' a)) '&' ('not' c)) 'or' ('not' (('not' b) 'or' d))) 'or' ('not' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:13
.= (((a '&' ('not' c)) 'or' (('not' ('not' b)) '&' ('not' d))) 'or' ('not' (('not' c) 'or' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:13
.= (((a '&' ('not' c)) 'or' (b '&' ('not' d))) 'or' (('not' ('not' c)) '&' ('not' ('not' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:13
.= ((a '&' ('not' c)) 'or' ((b '&' ('not' d)) 'or' (c '&' d))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:8
.= ((a '&' ('not' c)) 'or' ((b 'or' (c '&' d)) '&' (('not' d) 'or' (c '&' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:11
.= ((a '&' ('not' c)) 'or' ((b 'or' (c '&' d)) '&' ((('not' d) 'or' c) '&' (('not' d) 'or' d)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:11
.= ((a '&' ('not' c)) 'or' ((b 'or' (c '&' d)) '&' ((('not' d) 'or' c) '&' (I_el Y)))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_4:6
.= ((a '&' ('not' c)) 'or' ((b 'or' (c '&' d)) '&' (('not' d) 'or' c))) 'or' (('not' a) 'or' ('not' b)) by BVFUNC_1:6
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' ((a '&' ('not' c)) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:8
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' ((a 'or' (('not' a) 'or' ('not' b))) '&' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_1:11
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' (((a 'or' ('not' a)) 'or' ('not' b)) '&' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_1:8
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' (((I_el Y) 'or' ('not' b)) '&' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_4:6
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' ((I_el Y) '&' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_1:10
.= ((b 'or' (c '&' d)) '&' (('not' d) 'or' c)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:6
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' ((('not' d) 'or' c) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_1:11
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' (((('not' d) 'or' c) 'or' ('not' c)) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:8
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' ((('not' d) 'or' (c 'or' ('not' c))) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:8
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' ((('not' d) 'or' (I_el Y)) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_4:6
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' ((I_el Y) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:10
.= ((b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) '&' (I_el Y) by BVFUNC_1:10
.= (b 'or' (c '&' d)) 'or' (('not' c) 'or' (('not' a) 'or' ('not' b))) by BVFUNC_1:6
.= (c '&' d) 'or' (b 'or' (('not' c) 'or' (('not' a) 'or' ('not' b)))) by BVFUNC_1:8
.= (c '&' d) 'or' ((b 'or' (('not' b) 'or' ('not' a))) 'or' ('not' c)) by BVFUNC_1:8
.= (c '&' d) 'or' (((b 'or' ('not' b)) 'or' ('not' a)) 'or' ('not' c)) by BVFUNC_1:8
.= (c '&' d) 'or' (((I_el Y) 'or' ('not' a)) 'or' ('not' c)) by BVFUNC_4:6
.= (c '&' d) 'or' ((I_el Y) 'or' ('not' c)) by BVFUNC_1:10
.= (c '&' d) 'or' (I_el Y) by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ;
hence  ((((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE by BVFUNC_1:def_11; ::_thesis: verum
end;
hence  (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_8:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y
 for x being Element of Y holds ((a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c))) . x = TRUE
(a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = ('not' (a 'imp' b)) 'or' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' ((('not' a) 'or' (b 'imp' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' ((('not' a) 'or' (('not' b) 'or' c)) 'imp' (a 'imp' c)) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' ((('not' a) 'or' (('not' b) 'or' c)) 'imp' (('not' a) 'or' c)) by BVFUNC_4:8
.= ('not' (('not' a) 'or' b)) 'or' (('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' a) 'or' c)) by BVFUNC_4:8
.= (('not' ('not' a)) '&' ('not' b)) 'or' (('not' (('not' a) 'or' (('not' b) 'or' c))) 'or' (('not' a) 'or' c)) by BVFUNC_1:13
.= (('not' ('not' a)) '&' ('not' b)) 'or' ((('not' ('not' a)) '&' ('not' (('not' b) 'or' c))) 'or' (('not' a) 'or' c)) by BVFUNC_1:13
.= (a '&' ('not' b)) 'or' ((('not' ('not' a)) '&' (('not' ('not' b)) '&' ('not' c))) 'or' (('not' a) 'or' c)) by BVFUNC_1:13
.= (a '&' ('not' b)) 'or' ((a 'or' (('not' a) 'or' c)) '&' ((b '&' ('not' c)) 'or' (('not' a) 'or' c))) by BVFUNC_1:11
.= (a '&' ('not' b)) 'or' (((a 'or' ('not' a)) 'or' c) '&' ((b '&' ('not' c)) 'or' (('not' a) 'or' c))) by BVFUNC_1:8
.= (a '&' ('not' b)) 'or' (((I_el Y) 'or' c) '&' ((b '&' ('not' c)) 'or' (('not' a) 'or' c))) by BVFUNC_4:6
.= (a '&' ('not' b)) 'or' ((I_el Y) '&' ((b '&' ('not' c)) 'or' (('not' a) 'or' c))) by BVFUNC_1:10
.= (a '&' ('not' b)) 'or' ((b '&' ('not' c)) 'or' (('not' a) 'or' c)) by BVFUNC_1:6
.= (a '&' ('not' b)) 'or' ((b 'or' (('not' a) 'or' c)) '&' (('not' c) 'or' (('not' a) 'or' c))) by BVFUNC_1:11
.= (a '&' ('not' b)) 'or' ((b 'or' (('not' a) 'or' c)) '&' ((('not' c) 'or' c) 'or' ('not' a))) by BVFUNC_1:8
.= (a '&' ('not' b)) 'or' ((b 'or' (('not' a) 'or' c)) '&' ((I_el Y) 'or' ('not' a))) by BVFUNC_4:6
.= (a '&' ('not' b)) 'or' ((b 'or' (('not' a) 'or' c)) '&' (I_el Y)) by BVFUNC_1:10
.= (a '&' ('not' b)) 'or' (b 'or' (('not' a) 'or' c)) by BVFUNC_1:6
.= (a 'or' (b 'or' (('not' a) 'or' c))) '&' (('not' b) 'or' (b 'or' (('not' a) 'or' c))) by BVFUNC_1:11
.= (a 'or' (b 'or' (('not' a) 'or' c))) '&' ((('not' b) 'or' b) 'or' (('not' a) 'or' c)) by BVFUNC_1:8
.= (a 'or' (b 'or' (('not' a) 'or' c))) '&' ((I_el Y) 'or' (('not' a) 'or' c)) by BVFUNC_4:6
.= (a 'or' (b 'or' (('not' a) 'or' c))) '&' (I_el Y) by BVFUNC_1:10
.= a 'or' (b 'or' (('not' a) 'or' c)) by BVFUNC_1:6
.= a 'or' ((('not' a) 'or' b) 'or' c) by BVFUNC_1:8
.= (a 'or' (('not' a) 'or' b)) 'or' c by BVFUNC_1:8
.= ((a 'or' ('not' a)) 'or' b) 'or' c by BVFUNC_1:8
.= ((I_el Y) 'or' b) 'or' c by BVFUNC_4:6
.= (I_el Y) 'or' c by BVFUNC_1:10
.= I_el Y by BVFUNC_1:10 ;
hence  ((a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c))) . x = TRUE by BVFUNC_1:def_11; ::_thesis: verum
end;
hence  (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;