:: BVFUNC_6 semantic presentation

begin

theorem :: BVFUNC_6:1
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (b 'imp' (a '&' b)) = 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 '&' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b 'imp' (a '&' b)) = I_el Y
 for x being Element of Y holds (a 'imp' (b 'imp' (a '&' b))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (b 'imp' (a '&' b))) . x = TRUE
(a 'imp' (b 'imp' (a '&' b))) . x = ('not' (a . x)) 'or' ((b 'imp' (a '&' b)) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' ((a '&' b) . x)) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' ((a . x) '&' (b . x))) by MARGREL1:def_20
.= ('not' (a . x)) 'or' ((('not' (b . x)) 'or' (a . x)) '&' (('not' (b . x)) 'or' (b . x))) by XBOOLEAN:9
.= ('not' (a . x)) 'or' (TRUE '&' (('not' (b . x)) 'or' (a . x))) by XBOOLEAN:102
.= (('not' (a . x)) 'or' (a . x)) 'or' ('not' (b . x))
.= TRUE 'or' ('not' (b . x)) by XBOOLEAN:102
.= TRUE ;
hence  (a 'imp' (b 'imp' (a '&' b))) . x = TRUE ; ::_thesis: verum
end;
hence  a 'imp' (b 'imp' (a '&' b)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y
 for x being Element of Y holds ((a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b))) . x = TRUE
((a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b))) . x = ('not' ((a 'imp' b) . x)) 'or' (((b 'imp' a) 'imp' (a 'eqv' b)) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (b . x))) 'or' (((b 'imp' a) 'imp' (a 'eqv' b)) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (b . x))) 'or' (('not' ((b 'imp' a) . x)) 'or' ((a 'eqv' b) . x)) by BVFUNC_1:def_8
.= (('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' (('not' (('not' (b . x)) 'or' (a . x))) 'or' ((a 'eqv' b) . x)) by BVFUNC_1:def_8
.= ((a . x) '&' ('not' (b . x))) 'or' (((b . x) '&' ('not' (a . x))) 'or' ('not' ((a . x) 'xor' (b . x)))) by BVFUNC_1:def_9
.= ((a . x) '&' ('not' (b . x))) 'or' (((('not' (a . x)) '&' (b . x)) 'or' ('not' (('not' (a . x)) '&' (b . x)))) '&' ((('not' (a . x)) '&' (b . x)) 'or' ('not' ((a . x) '&' ('not' (b . x)))))) by XBOOLEAN:9
.= ((a . x) '&' ('not' (b . x))) 'or' (TRUE '&' ((('not' (a . x)) '&' (b . x)) 'or' ('not' ((a . x) '&' ('not' (b . x)))))) by XBOOLEAN:102
.= (((a . x) '&' ('not' (b . x))) 'or' ('not' ((a . x) '&' ('not' (b . x))))) 'or' (('not' (a . x)) '&' (b . x))
.= TRUE 'or' (('not' (a . x)) '&' (b . x)) by XBOOLEAN:102
.= TRUE ;
hence  ((a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b))) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'eqv' (b 'or' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'eqv' (b 'or' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) 'eqv' (b 'or' a) = I_el Y
 for x being Element of Y holds ((a 'or' b) 'eqv' (b 'or' a)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' b) 'eqv' (b 'or' a)) . x = TRUE
((a 'or' b) 'eqv' (b 'or' a)) . x = 'not' (((a 'or' b) . x) 'xor' ((b 'or' a) . x)) by BVFUNC_1:def_9
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'or' b) 'eqv' (b 'or' a)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' b) 'eqv' (b 'or' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:4
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y
 for x being Element of Y holds (((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c))) . x = TRUE
(((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c))) . x = ('not' (((a '&' b) 'imp' c) . x)) 'or' ((a 'imp' (b 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' ((a '&' b) . x)) 'or' (c . x))) 'or' ((a 'imp' (b 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' ((a . x) '&' (b . x))) 'or' (c . x))) 'or' ((a 'imp' (b 'imp' c)) . x) by MARGREL1:def_20
.= ('not' (('not' ((a . x) '&' (b . x))) 'or' (c . x))) 'or' (('not' (a . x)) 'or' ((b 'imp' c) . x)) by BVFUNC_1:def_8
.= ('not' ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x))) by BVFUNC_1:def_8
.= TRUE by XBOOLEAN:102 ;
hence  (((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c))) . x = TRUE ; ::_thesis: verum
end;
hence  ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:5
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a '&' b) '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' c)) 'imp' ((a '&' b) 'imp' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c) = I_el Y
 for x being Element of Y holds ((a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c)) . x = TRUE
((a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c)) . x = ('not' ((a 'imp' (b 'imp' c)) . x)) 'or' (((a '&' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' ((b 'imp' c) . x))) 'or' (((a '&' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' (((a '&' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' ((a '&' b) . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x)) by MARGREL1:def_20
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:6
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y
 for x being Element of Y holds ((c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b)))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b)))) . x = TRUE
((c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b)))) . x = ('not' ((c 'imp' a) . x)) 'or' (((c 'imp' b) 'imp' (c 'imp' (a '&' b))) . x) by BVFUNC_1:def_8
.= ('not' (('not' (c . x)) 'or' (a . x))) 'or' (((c 'imp' b) 'imp' (c 'imp' (a '&' b))) . x) by BVFUNC_1:def_8
.= ('not' (('not' (c . x)) 'or' (a . x))) 'or' (('not' ((c 'imp' b) . x)) 'or' ((c 'imp' (a '&' b)) . x)) by BVFUNC_1:def_8
.= ('not' (('not' (c . x)) 'or' (a . x))) 'or' (('not' (('not' (c . x)) 'or' (b . x))) 'or' ((c 'imp' (a '&' b)) . x)) by BVFUNC_1:def_8
.= ('not' (('not' (c . x)) 'or' (a . x))) 'or' (('not' (('not' (c . x)) 'or' (b . x))) 'or' (('not' (c . x)) 'or' ((a '&' b) . x))) by BVFUNC_1:def_8
.= ((c . x) '&' ('not' (a . x))) 'or' ((('not' ('not' (c . x))) '&' ('not' (b . x))) 'or' (('not' (c . x)) 'or' ((a . x) '&' (b . x)))) by MARGREL1:def_20
.= ((c . x) '&' ('not' (a . x))) 'or' (((c . x) '&' ('not' (b . x))) 'or' ((('not' (c . x)) 'or' (a . x)) '&' (('not' (c . x)) 'or' (b . x)))) by XBOOLEAN:9
.= ((c . x) '&' ('not' (a . x))) 'or' ((((c . x) '&' ('not' (b . x))) 'or' (('not' (c . x)) 'or' (a . x))) '&' (((c . x) '&' ('not' (b . x))) 'or' (('not' (c . x)) 'or' ('not' ('not' (b . x)))))) by XBOOLEAN:9
.= ((c . x) '&' ('not' (a . x))) 'or' (TRUE '&' (((c . x) '&' ('not' (b . x))) 'or' (('not' (c . x)) 'or' (a . x)))) by XBOOLEAN:102
.= (((c . x) '&' ('not' (a . x))) 'or' ('not' ((c . x) '&' ('not' (a . x))))) 'or' ((c . x) '&' ('not' (b . x)))
.= TRUE 'or' ((c . x) '&' ('not' (b . x))) by XBOOLEAN:102
.= TRUE ;
hence  ((c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b)))) . x = TRUE ; ::_thesis: verum
end;
hence  (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:7
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y
 for x being Element of Y holds (((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c))) . x = TRUE
(((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c))) . x = ('not' (((a 'or' b) 'imp' c) . x)) 'or' (((a 'imp' c) 'or' (b 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' ((a 'or' b) . x)) 'or' (c . x))) 'or' (((a 'imp' c) 'or' (b 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' ((a . x) 'or' (b . x))) 'or' (c . x))) 'or' (((a 'imp' c) 'or' (b 'imp' c)) . x) by BVFUNC_1:def_4
.= ('not' (('not' ((a . x) 'or' (b . x))) 'or' (c . x))) 'or' (((a 'imp' c) . x) 'or' ((b 'imp' c) . x)) by BVFUNC_1:def_4
.= ('not' (('not' ((a . x) 'or' (b . x))) 'or' (c . x))) 'or' ((('not' (a . x)) 'or' (c . x)) 'or' ((b 'imp' c) . x)) by BVFUNC_1:def_8
.= (('not' ('not' ((a . x) 'or' (b . x)))) '&' ('not' (c . x))) 'or' ((('not' (a . x)) 'or' (c . x)) 'or' (('not' (b . x)) 'or' (c . x))) by BVFUNC_1:def_8
.= (((b . x) '&' ('not' (c . x))) 'or' ((a . x) '&' ('not' (c . x)))) 'or' (('not' ((a . x) '&' ('not' (c . x)))) 'or' (('not' (b . x)) 'or' (c . x))) by XBOOLEAN:8
.= (((b . x) '&' ('not' (c . x))) 'or' (((a . x) '&' ('not' (c . x))) 'or' ('not' ((a . x) '&' ('not' (c . x)))))) 'or' (('not' (b . x)) 'or' (c . x))
.= (((b . x) '&' ('not' (c . x))) 'or' TRUE) 'or' (('not' (b . x)) 'or' (c . x)) by XBOOLEAN:102
.= TRUE ;
hence  (((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c))) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) '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' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) = I_el Y
 for x being Element of Y holds ((a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c))) . x = TRUE
((a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c))) . x = ('not' ((a 'imp' c) . x)) 'or' (((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' ((b 'imp' c) . x)) 'or' (((a 'or' b) 'imp' c) . x)) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (((a 'or' b) 'imp' c) . x)) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' ((a 'or' b) . x)) 'or' (c . x))) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' ((a . x) 'or' (b . x))) 'or' (c . x))) by BVFUNC_1:def_4
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (((c . x) 'or' ('not' (a . x))) '&' (('not' (b . x)) 'or' (c . x)))) by XBOOLEAN:9
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' ((('not' (('not' (b . x)) 'or' (c . x))) 'or' ((c . x) 'or' ('not' (a . x)))) '&' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (b . x)) 'or' (c . x)))) by XBOOLEAN:9
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (TRUE '&' (('not' (('not' (b . x)) 'or' (c . x))) 'or' ((c . x) 'or' ('not' (a . x))))) by XBOOLEAN:102
.= ('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (c . x)))
.= (('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (('not' (b . x)) 'or' (c . x)))
.= TRUE 'or' ('not' (('not' (b . x)) 'or' (c . x))) by XBOOLEAN:102
.= TRUE ;
hence  ((a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c))) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) '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' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y
 for x being Element of Y holds (((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c)) . x = TRUE
(((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c)) . x = ('not' (((a 'imp' c) '&' (b 'imp' c)) . x)) 'or' (((a 'or' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' (((a 'imp' c) . x) '&' ((b 'imp' c) . x))) 'or' (((a 'or' b) 'imp' c) . x) by MARGREL1:def_20
.= ('not' ((('not' (a . x)) 'or' (c . x)) '&' ((b 'imp' c) . x))) 'or' (((a 'or' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' ((('not' (a . x)) 'or' (c . x)) '&' (('not' (b . x)) 'or' (c . x)))) 'or' (((a 'or' b) 'imp' c) . x) by BVFUNC_1:def_8
.= ('not' ((('not' (a . x)) 'or' (c . x)) '&' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' ((a 'or' b) . x)) 'or' (c . x)) by BVFUNC_1:def_8
.= (('not' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (('not' (b . x)) 'or' (c . x)))) 'or' ((c . x) 'or' ('not' ((a . x) 'or' (b . x)))) by BVFUNC_1:def_4
.= (('not' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (('not' (b . x)) 'or' (c . x)))) 'or' ((('not' (a . x)) 'or' (c . x)) '&' ((c . x) 'or' ('not' (b . x)))) by XBOOLEAN:9
.= ((('not' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' (a . x)) 'or' (c . x))) '&' ((('not' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' (b . x)) 'or' (c . x))) by XBOOLEAN:9
.= (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (a . x)) 'or' (c . x)))) '&' (('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (b . x)) 'or' (c . x))))
.= (('not' (('not' (b . x)) 'or' (c . x))) 'or' TRUE) '&' (('not' (('not' (a . x)) 'or' (c . x))) 'or' (('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (b . x)) 'or' (c . x)))) by XBOOLEAN:102
.= TRUE '&' (('not' (('not' (a . x)) 'or' (c . x))) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c)) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:10
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' (b '&' ('not' b))) 'imp' ('not' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' (b '&' ('not' b))) 'imp' ('not' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' (b '&' ('not' b))) 'imp' ('not' a) = I_el Y
 for x being Element of Y holds ((a 'imp' (b '&' ('not' b))) 'imp' ('not' a)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' (b '&' ('not' b))) 'imp' ('not' a)) . x = TRUE
((a 'imp' (b '&' ('not' b))) 'imp' ('not' a)) . x = ('not' ((a 'imp' (b '&' ('not' b))) . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' ((b '&' ('not' b)) . x))) 'or' (('not' a) . x) by BVFUNC_1:def_8
.= ((a . x) '&' (('not' (b . x)) 'or' ('not' (('not' b) . x)))) 'or' (('not' a) . x) by MARGREL1:def_20
.= ((a . x) '&' (('not' (b . x)) 'or' ('not' ('not' (b . x))))) 'or' (('not' a) . x) by MARGREL1:def_19
.= ((a . x) '&' TRUE) 'or' (('not' a) . x) by XBOOLEAN:102
.= (a . x) 'or' ('not' (a . x)) by MARGREL1:def_19
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'imp' (b '&' ('not' b))) 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' (b '&' ('not' b))) 'imp' ('not' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

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

theorem :: BVFUNC_6:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y
 for x being Element of Y holds ((a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c))) . x = TRUE
((a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c))) . x = ('not' ((a '&' (b 'or' c)) . x)) 'or' (((a '&' b) 'or' (a '&' c)) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) '&' ((b 'or' c) . x))) 'or' (((a '&' b) 'or' (a '&' c)) . x) by MARGREL1:def_20
.= ('not' ((a . x) '&' ((b . x) 'or' (c . x)))) 'or' (((a '&' b) 'or' (a '&' c)) . x) by BVFUNC_1:def_4
.= ('not' ((a . x) '&' ((b . x) 'or' (c . x)))) 'or' (((a '&' b) . x) 'or' ((a '&' c) . x)) by BVFUNC_1:def_4
.= ('not' ((a . x) '&' ((b . x) 'or' (c . x)))) 'or' (((a . x) '&' (b . x)) 'or' ((a '&' c) . x)) by MARGREL1:def_20
.= ('not' ((a . x) '&' ((b . x) 'or' (c . x)))) 'or' (((a . x) '&' (b . x)) 'or' ((a . x) '&' (c . x))) by MARGREL1:def_20
.= (((a . x) '&' (b . x)) 'or' ((a . x) '&' (c . x))) 'or' (('not' ((a . x) '&' (b . x))) '&' ('not' ((a . x) '&' (c . x)))) by XBOOLEAN:8
.= ((((a . x) '&' (c . x)) 'or' ((a . x) '&' (b . x))) 'or' ('not' ((a . x) '&' (b . x)))) '&' ((((a . x) '&' (b . x)) 'or' ((a . x) '&' (c . x))) 'or' ('not' ((a . x) '&' (c . x)))) by XBOOLEAN:9
.= (((a . x) '&' (c . x)) 'or' (((a . x) '&' (b . x)) 'or' ('not' ((a . x) '&' (b . x))))) '&' (((a . x) '&' (b . x)) 'or' (((a . x) '&' (c . x)) 'or' ('not' ((a . x) '&' (c . x)))))
.= (((a . x) '&' (c . x)) 'or' TRUE) '&' (((a . x) '&' (b . x)) 'or' (((a . x) '&' (c . x)) 'or' ('not' ((a . x) '&' (c . x))))) by XBOOLEAN:102
.= TRUE '&' (((a . x) '&' (b . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c))) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:13
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y
 for x being Element of Y holds (((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c)) . x = TRUE
(((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c)) . x = ('not' (((a 'or' c) '&' (b 'or' c)) . x)) 'or' (((a '&' b) 'or' c) . x) by BVFUNC_1:def_8
.= ('not' (((a 'or' c) . x) '&' ((b 'or' c) . x))) 'or' (((a '&' b) 'or' c) . x) by MARGREL1:def_20
.= ('not' (((a . x) 'or' (c . x)) '&' ((b 'or' c) . x))) 'or' (((a '&' b) 'or' c) . x) by BVFUNC_1:def_4
.= (('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' (((a '&' b) 'or' c) . x) by BVFUNC_1:def_4
.= (('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' (((a '&' b) . x) 'or' (c . x)) by BVFUNC_1:def_4
.= (('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' ((c . x) 'or' ((a . x) '&' (b . x))) by MARGREL1:def_20
.= (('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' (((a . x) 'or' (c . x)) '&' ((c . x) 'or' (b . x))) by XBOOLEAN:9
.= ((('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' ((a . x) 'or' (c . x))) '&' ((('not' ((a . x) 'or' (c . x))) 'or' ('not' ((b . x) 'or' (c . x)))) 'or' ((b . x) 'or' (c . x))) by XBOOLEAN:9
.= (('not' ((b . x) 'or' (c . x))) 'or' (('not' ((a . x) 'or' (c . x))) 'or' ((a . x) 'or' (c . x)))) '&' (('not' ((a . x) 'or' (c . x))) 'or' (('not' ((b . x) 'or' (c . x))) 'or' ((b . x) 'or' (c . x))))
.= (('not' ((b . x) 'or' (c . x))) 'or' TRUE) '&' (('not' ((a . x) 'or' (c . x))) 'or' (('not' ((b . x) 'or' (c . x))) 'or' ((b . x) 'or' (c . x)))) by XBOOLEAN:102
.= TRUE '&' (('not' ((a . x) 'or' (c . x))) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c)) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:14
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y
 for x being Element of Y holds (((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c))) . x = TRUE
(((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c))) . x = ('not' (((a 'or' b) '&' c) . x)) 'or' (((a '&' c) 'or' (b '&' c)) . x) by BVFUNC_1:def_8
.= ('not' (((a 'or' b) . x) '&' (c . x))) 'or' (((a '&' c) 'or' (b '&' c)) . x) by MARGREL1:def_20
.= ('not' (((a . x) 'or' (b . x)) '&' (c . x))) 'or' (((a '&' c) 'or' (b '&' c)) . x) by BVFUNC_1:def_4
.= ('not' (((a . x) 'or' (b . x)) '&' (c . x))) 'or' (((a '&' c) . x) 'or' ((b '&' c) . x)) by BVFUNC_1:def_4
.= ('not' (((a . x) 'or' (b . x)) '&' (c . x))) 'or' (((a . x) '&' (c . x)) 'or' ((b '&' c) . x)) by MARGREL1:def_20
.= ('not' ((c . x) '&' ((a . x) 'or' (b . x)))) 'or' (((a . x) '&' (c . x)) 'or' ((b . x) '&' (c . x))) by MARGREL1:def_20
.= (((a . x) '&' (c . x)) 'or' ((b . x) '&' (c . x))) 'or' (('not' ((a . x) '&' (c . x))) '&' ('not' ((b . x) '&' (c . x)))) by XBOOLEAN:8
.= ((((b . x) '&' (c . x)) 'or' ((a . x) '&' (c . x))) 'or' ('not' ((a . x) '&' (c . x)))) '&' ((((a . x) '&' (c . x)) 'or' ((b . x) '&' (c . x))) 'or' ('not' ((b . x) '&' (c . x)))) by XBOOLEAN:9
.= (((b . x) '&' (c . x)) 'or' (((a . x) '&' (c . x)) 'or' ('not' ((a . x) '&' (c . x))))) '&' (((a . x) '&' (c . x)) 'or' (((b . x) '&' (c . x)) 'or' ('not' ((b . x) '&' (c . x)))))
.= (((b . x) '&' (c . x)) 'or' TRUE) '&' (((a . x) '&' (c . x)) 'or' (((b . x) '&' (c . x)) 'or' ('not' ((b . x) '&' (c . x))))) by XBOOLEAN:102
.= TRUE '&' (((a . x) '&' (c . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c))) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:15
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '&' b = I_el Y holds
a 'or' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a '&' b = I_el Y holds
a 'or' b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a '&' b = I_el Y implies a 'or' b = I_el Y )
assume A1: a '&' b = I_el Y ; ::_thesis: a 'or' b = I_el Y
 for x being Element of Y holds (a 'or' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'or' b) . x = TRUE
 (a '&' b) . x = TRUE by A1, BVFUNC_1:def_11;
then A2: (a . x) '&' (b . x) = TRUE by MARGREL1:def_20;
then  a . x = TRUE by MARGREL1:12;
then (a 'or' b) . x = TRUE 'or' TRUE by A2, BVFUNC_1:def_4
.= TRUE ;
hence  (a 'or' b) . x = TRUE ; ::_thesis: verum
end;
hence  a 'or' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:16
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a 'or' c) 'imp' (b 'or' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a 'or' c) 'imp' (b 'or' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y implies (a 'or' c) 'imp' (b 'or' c) = I_el Y )
assume A1: a 'imp' b = I_el Y ; ::_thesis: (a 'or' c) 'imp' (b 'or' c) = I_el Y
 for x being Element of Y holds ((a 'or' c) 'imp' (b 'or' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' c) 'imp' (b 'or' c)) . x = TRUE
 (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11;
then A2: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
((a 'or' c) 'imp' (b 'or' c)) . x = ('not' ((a 'or' c) . x)) 'or' ((b 'or' c) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' (c . x))) 'or' ((b 'or' c) . x) by BVFUNC_1:def_4
.= ((b . x) 'or' (c . x)) 'or' (('not' (a . x)) '&' ('not' (c . x))) by BVFUNC_1:def_4
.= (((c . x) 'or' (b . x)) 'or' ('not' (a . x))) '&' (((b . x) 'or' (c . x)) 'or' ('not' (c . x))) by XBOOLEAN:9
.= ((c . x) 'or' (('not' (a . x)) 'or' (b . x))) '&' (((b . x) 'or' (c . x)) 'or' ('not' (c . x)))
.= TRUE '&' ((b . x) 'or' ((c . x) 'or' ('not' (c . x)))) by A2
.= TRUE '&' ((b . x) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  ((a 'or' c) 'imp' (b 'or' c)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' c) 'imp' (b 'or' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:17
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a '&' c) 'imp' (b '&' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a '&' c) 'imp' (b '&' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y implies (a '&' c) 'imp' (b '&' c) = I_el Y )
assume A1: a 'imp' b = I_el Y ; ::_thesis: (a '&' c) 'imp' (b '&' c) = I_el Y
 for x being Element of Y holds ((a '&' c) 'imp' (b '&' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' c) 'imp' (b '&' c)) . x = TRUE
 (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11;
then A2: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
((a '&' c) 'imp' (b '&' c)) . x = ('not' ((a '&' c) . x)) 'or' ((b '&' c) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) '&' (c . x))) 'or' ((b '&' c) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) '&' (c . x)) by MARGREL1:def_20
.= ((('not' (c . x)) 'or' ('not' (a . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (c . x)) by XBOOLEAN:9
.= (('not' (c . x)) 'or' (('not' (a . x)) 'or' (b . x))) '&' (('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x)))
.= (('not' (c . x)) 'or' (('not' (a . x)) 'or' (b . x))) '&' (('not' (a . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE by A2 ;
hence  ((a '&' c) 'imp' (b '&' c)) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' c) 'imp' (b '&' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a '&' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a '&' b) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( c 'imp' a = I_el Y & c 'imp' b = I_el Y implies c 'imp' (a '&' b) = I_el Y )
assume that
A1: c 'imp' a = I_el Y and
A2: c 'imp' b = I_el Y ; ::_thesis: c 'imp' (a '&' b) = I_el Y
 for x being Element of Y holds (c 'imp' (a '&' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (c 'imp' (a '&' b)) . x = TRUE
 (c 'imp' a) . x = TRUE by A1, BVFUNC_1:def_11;
then A3: ('not' (c . x)) 'or' (a . x) = TRUE by BVFUNC_1:def_8;
 (c 'imp' b) . x = TRUE by A2, BVFUNC_1:def_11;
then A4: ('not' (c . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
(c 'imp' (a '&' b)) . x = ('not' (c . x)) 'or' ((a '&' b) . x) by BVFUNC_1:def_8
.= ('not' (c . x)) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_20
.= TRUE '&' TRUE by A3, A4, XBOOLEAN:9
.= TRUE ;
hence  (c 'imp' (a '&' b)) . x = TRUE ; ::_thesis: verum
end;
hence  c 'imp' (a '&' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a 'or' b) 'imp' c = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a 'or' b) 'imp' c = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a 'or' b) 'imp' c = I_el Y )
assume that
A1: a 'imp' c = I_el Y and
A2: b 'imp' c = I_el Y ; ::_thesis: (a 'or' b) 'imp' c = I_el Y
 for x being Element of Y holds ((a 'or' b) 'imp' c) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' b) 'imp' c) . x = TRUE
 (a 'imp' c) . x = TRUE by A1, BVFUNC_1:def_11;
then A3: ('not' (a . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
 (b 'imp' c) . x = TRUE by A2, BVFUNC_1:def_11;
then A4: ('not' (b . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8;
((a 'or' b) 'imp' c) . x = ('not' ((a 'or' b) . x)) 'or' (c . x) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' (b . x))) 'or' (c . x) by BVFUNC_1:def_4
.= TRUE '&' TRUE by A3, A4, XBOOLEAN:9
.= TRUE ;
hence  ((a 'or' b) 'imp' c) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' b) 'imp' c = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:20
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'or' b = I_el Y & 'not' a = I_el Y holds
b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a 'or' b = I_el Y & 'not' a = I_el Y holds
b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'or' b = I_el Y & 'not' a = I_el Y implies b = I_el Y )
assume that
A1: a 'or' b = I_el Y and
A2: 'not' a = I_el Y ; ::_thesis: b = I_el Y
 for x being Element of Y holds b . x = TRUE
proof
let x be Element of Y; ::_thesis: b . x = TRUE
 ('not' a) . x = TRUE by A2, BVFUNC_1:def_11;
then A3: 'not' (a . x) = TRUE by MARGREL1:def_19;
 (a 'or' b) . x = TRUE by A1, BVFUNC_1:def_11;
then  (a . x) 'or' (b . x) = TRUE by BVFUNC_1:def_4;
hence  b . x = TRUE by A3; ::_thesis: verum
end;
hence  b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:21
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a '&' c) 'imp' (b '&' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a '&' c) 'imp' (b '&' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y & c 'imp' d = I_el Y implies (a '&' c) 'imp' (b '&' d) = I_el Y )
assume that
A1: a 'imp' b = I_el Y and
A2: c 'imp' d = I_el Y ; ::_thesis: (a '&' c) 'imp' (b '&' d) = I_el Y
 for x being Element of Y holds ((a '&' c) 'imp' (b '&' d)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' c) 'imp' (b '&' d)) . x = TRUE
 (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11;
then A3: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
 (c 'imp' d) . x = TRUE by A2, BVFUNC_1:def_11;
then A4: ('not' (c . x)) 'or' (d . x) = TRUE by BVFUNC_1:def_8;
((a '&' c) 'imp' (b '&' d)) . x = ('not' ((a '&' c) . x)) 'or' ((b '&' d) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) '&' (c . x))) 'or' ((b '&' d) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) '&' (d . x)) by MARGREL1:def_20
.= ((('not' (c . x)) 'or' ('not' (a . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (d . x)) by XBOOLEAN:9
.= (('not' (c . x)) 'or' (('not' (a . x)) 'or' (b . x))) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (d . x))
.= TRUE '&' (('not' (a . x)) 'or' TRUE) by A3, A4, BINARITH:11
.= TRUE ;
hence  ((a '&' c) 'imp' (b '&' d)) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' c) 'imp' (b '&' d) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:22
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a 'or' c) 'imp' (b 'or' d) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a 'or' c) 'imp' (b 'or' d) = I_el Y
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y & c 'imp' d = I_el Y implies (a 'or' c) 'imp' (b 'or' d) = I_el Y )
assume that
A1: a 'imp' b = I_el Y and
A2: c 'imp' d = I_el Y ; ::_thesis: (a 'or' c) 'imp' (b 'or' d) = I_el Y
 for x being Element of Y holds ((a 'or' c) 'imp' (b 'or' d)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' c) 'imp' (b 'or' d)) . x = TRUE
 (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11;
then A3: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
 (c 'imp' d) . x = TRUE by A2, BVFUNC_1:def_11;
then A4: ('not' (c . x)) 'or' (d . x) = TRUE by BVFUNC_1:def_8;
((a 'or' c) 'imp' (b 'or' d)) . x = ('not' ((a 'or' c) . x)) 'or' ((b 'or' d) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' (c . x))) 'or' ((b 'or' d) . x) by BVFUNC_1:def_4
.= ((b . x) 'or' (d . x)) 'or' (('not' (a . x)) '&' ('not' (c . x))) by BVFUNC_1:def_4
.= (((d . x) 'or' (b . x)) 'or' ('not' (a . x))) '&' (((b . x) 'or' (d . x)) 'or' ('not' (c . x))) by XBOOLEAN:9
.= ((d . x) 'or' ((b . x) 'or' ('not' (a . x)))) '&' (((b . x) 'or' (d . x)) 'or' ('not' (c . x)))
.= TRUE '&' ((b . x) 'or' TRUE) by A3, A4, BINARITH:11
.= TRUE ;
hence  ((a 'or' c) 'imp' (b 'or' d)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' c) 'imp' (b 'or' d) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:23
for Y being non empty set
for a, b being Function of Y,BOOLEAN st (a '&' ('not' b)) 'imp' ('not' a) = I_el Y holds
a 'imp' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st (a '&' ('not' b)) 'imp' ('not' a) = I_el Y holds
a 'imp' b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( (a '&' ('not' b)) 'imp' ('not' a) = I_el Y implies a 'imp' b = I_el Y )
assume A1: (a '&' ('not' b)) 'imp' ('not' a) = I_el Y ; ::_thesis: a 'imp' b = I_el Y
 for x being Element of Y holds (a 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' b) . x = TRUE
 ((a '&' ('not' b)) 'imp' ('not' a)) . x = TRUE by A1, BVFUNC_1:def_11;
then  ('not' ((a '&' ('not' b)) . x)) 'or' (('not' a) . x) = TRUE by BVFUNC_1:def_8;
then  ('not' ((a . x) '&' (('not' b) . x))) 'or' (('not' a) . x) = TRUE by MARGREL1:def_20;
then  (('not' (a . x)) 'or' ('not' ('not' (b . x)))) 'or' (('not' a) . x) = TRUE by MARGREL1:def_19;
then  (('not' (a . x)) 'or' (b . x)) 'or' ('not' (a . x)) = TRUE by MARGREL1:def_19;
then  (b . x) 'or' (('not' (a . x)) 'or' ('not' (a . x))) = TRUE by XBOOLEAN:4;
hence  (a 'imp' b) . x = TRUE by BVFUNC_1:def_8; ::_thesis: verum
end;
hence  a 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:24
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'imp' ('not' b) = I_el Y holds
b 'imp' ('not' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a 'imp' ('not' b) = I_el Y holds
b 'imp' ('not' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' ('not' b) = I_el Y implies b 'imp' ('not' a) = I_el Y )
assume A1: a 'imp' ('not' b) = I_el Y ; ::_thesis: b 'imp' ('not' a) = I_el Y
 for x being Element of Y holds (b 'imp' ('not' a)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (b 'imp' ('not' a)) . x = TRUE
 (a 'imp' ('not' b)) . x = TRUE by A1, BVFUNC_1:def_11;
then  ('not' (a . x)) 'or' (('not' b) . x) = TRUE by BVFUNC_1:def_8;
then A2: ('not' (a . x)) 'or' ('not' (b . x)) = TRUE by MARGREL1:def_19;
(b 'imp' ('not' a)) . x = ('not' (b . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8
.= TRUE by A2, MARGREL1:def_19 ;
hence  (b 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum
end;
hence  b 'imp' ('not' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:25
for Y being non empty set
for a, b being Function of Y,BOOLEAN st ('not' a) 'imp' b = I_el Y holds
('not' b) 'imp' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st ('not' a) 'imp' b = I_el Y holds
('not' b) 'imp' a = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ( ('not' a) 'imp' b = I_el Y implies ('not' b) 'imp' a = I_el Y )
assume A1: ('not' a) 'imp' b = I_el Y ; ::_thesis: ('not' b) 'imp' a = I_el Y
 for x being Element of Y holds (('not' b) 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: (('not' b) 'imp' a) . x = TRUE
 (('not' a) 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11;
then  ('not' (('not' a) . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8;
then A2: ('not' ('not' (a . x))) 'or' (b . x) = TRUE by MARGREL1:def_19;
(('not' b) 'imp' a) . x = ('not' (('not' b) . x)) 'or' (a . x) by BVFUNC_1:def_8
.= TRUE by A2, MARGREL1:def_19 ;
hence  (('not' b) 'imp' a) . x = TRUE ; ::_thesis: verum
end;
hence  ('not' b) 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:26
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'or' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'or' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' (a 'or' b) = I_el Y
 for x being Element of Y holds (a 'imp' (a 'or' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (a 'or' b)) . x = TRUE
(a 'imp' (a 'or' b)) . x = ('not' (a . x)) 'or' ((a 'or' b) . x) by BVFUNC_1:def_8
.= ('not' (a . x)) 'or' ((a . x) 'or' (b . x)) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (a . x)) 'or' (b . x)
.= TRUE 'or' (b . x) by XBOOLEAN:102
.= TRUE ;
hence  (a 'imp' (a 'or' b)) . x = TRUE ; ::_thesis: verum
end;
hence  a 'imp' (a 'or' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:27
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'imp' (('not' a) 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'imp' (('not' a) 'imp' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) 'imp' (('not' a) 'imp' b) = I_el Y
 for x being Element of Y holds ((a 'or' b) 'imp' (('not' a) 'imp' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' b) 'imp' (('not' a) 'imp' b)) . x = TRUE
((a 'or' b) 'imp' (('not' a) 'imp' b)) . x = ('not' ((a 'or' b) . x)) 'or' ((('not' a) 'imp' b) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' (b . x))) 'or' ((('not' a) 'imp' b) . x) by BVFUNC_1:def_4
.= (('not' (a . x)) '&' ('not' (b . x))) 'or' (('not' (('not' a) . x)) 'or' (b . x)) by BVFUNC_1:def_8
.= ((a . x) 'or' (b . x)) 'or' (('not' (a . x)) '&' ('not' (b . x))) by MARGREL1:def_19
.= (((a . x) 'or' (b . x)) 'or' ('not' (a . x))) '&' (((a . x) 'or' (b . x)) 'or' ('not' (b . x))) by XBOOLEAN:9
.= (((a . x) 'or' ('not' (a . x))) 'or' (b . x)) '&' ((a . x) 'or' ((b . x) 'or' ('not' (b . x))))
.= (TRUE 'or' (b . x)) '&' ((a . x) 'or' ((b . x) 'or' ('not' (b . x)))) by XBOOLEAN:102
.= TRUE '&' ((a . x) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  ((a 'or' b) 'imp' (('not' a) 'imp' b)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' b) 'imp' (('not' a) 'imp' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem Th28: :: BVFUNC_6:28
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) = I_el Y
 for x being Element of Y holds (('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b))) . x = TRUE
(('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b))) . x = ('not' (('not' (a 'or' b)) . x)) 'or' ((('not' a) '&' ('not' b)) . x) by BVFUNC_1:def_8
.= ((a 'or' b) . x) 'or' ((('not' a) '&' ('not' b)) . x) by MARGREL1:def_19
.= ((a . x) 'or' (b . x)) 'or' ((('not' a) '&' ('not' b)) . x) by BVFUNC_1:def_4
.= ((a . x) 'or' (b . x)) 'or' ((('not' a) . x) '&' (('not' b) . x)) by MARGREL1:def_20
.= ((a . x) 'or' (b . x)) 'or' (('not' (a . x)) '&' (('not' b) . x)) by MARGREL1:def_19
.= ((a . x) 'or' (b . x)) 'or' (('not' (a . x)) '&' ('not' (b . x))) by MARGREL1:def_19
.= (((a . x) 'or' (b . x)) 'or' ('not' (a . x))) '&' (((a . x) 'or' (b . x)) 'or' ('not' (b . x))) by XBOOLEAN:9
.= (((a . x) 'or' ('not' (a . x))) 'or' (b . x)) '&' ((a . x) 'or' ((b . x) 'or' ('not' (b . x))))
.= (TRUE 'or' (b . x)) '&' ((a . x) 'or' ((b . x) 'or' ('not' (b . x)))) by XBOOLEAN:102
.= TRUE '&' ((a . x) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b))) . x = TRUE ; ::_thesis: verum
end;
hence  ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:29
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (('not' a) '&' ('not' b)) 'imp' ('not' (a 'or' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (('not' a) '&' ('not' b)) 'imp' ('not' (a 'or' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (('not' a) '&' ('not' b)) 'imp' ('not' (a 'or' b)) = I_el Y
thus (('not' a) '&' ('not' b)) 'imp' ('not' (a 'or' b)) = ('not' (a 'or' b)) 'imp' ('not' (a 'or' b)) by BVFUNC_1:13
.= ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) by BVFUNC_1:13
.= I_el Y by Th28 ; ::_thesis: verum
end;

theorem :: BVFUNC_6:30
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' ('not' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' ('not' a) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' (a 'or' b)) 'imp' ('not' a) = I_el Y
 for x being Element of Y holds (('not' (a 'or' b)) 'imp' ('not' a)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (('not' (a 'or' b)) 'imp' ('not' a)) . x = TRUE
(('not' (a 'or' b)) 'imp' ('not' a)) . x = ('not' (('not' (a 'or' b)) . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8
.= ('not' ('not' ((a 'or' b) . x))) 'or' (('not' a) . x) by MARGREL1:def_19
.= ((a 'or' b) . x) 'or' ('not' (a . x)) by MARGREL1:def_19
.= ((a . x) 'or' (b . x)) 'or' ('not' (a . x)) by BVFUNC_1:def_4
.= ((a . x) 'or' ('not' (a . x))) 'or' (b . x)
.= TRUE 'or' (b . x) by XBOOLEAN:102
.= TRUE ;
hence  (('not' (a 'or' b)) 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum
end;
hence  ('not' (a 'or' b)) 'imp' ('not' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:31
for Y being non empty set
for a being Function of Y,BOOLEAN holds (a 'or' a) 'imp' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (a 'or' a) 'imp' a = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: (a 'or' a) 'imp' a = I_el Y
 for x being Element of Y holds ((a 'or' a) 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' a) 'imp' a) . x = TRUE
((a 'or' a) 'imp' a) . x = ('not' (a . x)) 'or' (a . x) by BVFUNC_1:def_8
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'or' a) 'imp' a) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' a) 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:32
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' ('not' a)) 'imp' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' ('not' a)) 'imp' b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' ('not' a)) 'imp' b = I_el Y
 for x being Element of Y holds ((a '&' ('not' a)) 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' ('not' a)) 'imp' b) . x = TRUE
((a '&' ('not' a)) 'imp' b) . x = ('not' ((a '&' ('not' a)) . x)) 'or' (b . x) by BVFUNC_1:def_8
.= ('not' ((a . x) '&' (('not' a) . x))) 'or' (b . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' ('not' ('not' (a . x)))) 'or' (b . x) by MARGREL1:def_19
.= TRUE 'or' (b . x) by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' ('not' a)) 'imp' b) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' ('not' a)) 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:33
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' a) 'or' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' a) 'or' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (('not' a) 'or' b) = I_el Y
 for x being Element of Y holds ((a 'imp' b) 'imp' (('not' a) 'or' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'imp' b) 'imp' (('not' a) 'or' b)) . x = TRUE
((a 'imp' b) 'imp' (('not' a) 'or' b)) . x = ('not' ((a 'imp' b) . x)) 'or' ((('not' a) 'or' b) . x) by BVFUNC_1:def_8
.= ('not' (('not' (a . x)) 'or' (b . x))) 'or' ((('not' a) 'or' b) . x) by BVFUNC_1:def_8
.= (('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' ((('not' a) . x) 'or' (b . x)) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) by MARGREL1:def_19
.= ((('not' (a . x)) 'or' (b . x)) 'or' (a . x)) '&' ((('not' (a . x)) 'or' (b . x)) 'or' ('not' (b . x))) by XBOOLEAN:9
.= ((('not' (a . x)) 'or' (a . x)) 'or' (b . x)) '&' (('not' (a . x)) 'or' ((b . x) 'or' ('not' (b . x))))
.= (TRUE 'or' (b . x)) '&' (('not' (a . x)) 'or' ((b . x) 'or' ('not' (b . x)))) by XBOOLEAN:102
.= TRUE '&' (('not' (a . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  ((a 'imp' b) 'imp' (('not' a) 'or' b)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' b) 'imp' (('not' a) 'or' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:34
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y
 for x being Element of Y holds ((a '&' b) 'imp' ('not' (a 'imp' ('not' b)))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' b) 'imp' ('not' (a 'imp' ('not' b)))) . x = TRUE
((a '&' b) 'imp' ('not' (a 'imp' ('not' b)))) . x = ('not' ((a '&' b) . x)) 'or' (('not' (a 'imp' ('not' b))) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) '&' (b . x))) 'or' (('not' (a 'imp' ('not' b))) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ('not' ((a 'imp' ('not' b)) . x)) by MARGREL1:def_19
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ('not' (('not' (a . x)) 'or' (('not' b) . x))) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19
.= ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (a . x)) '&' ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (b . x)) by XBOOLEAN:9
.= ((('not' (a . x)) 'or' (a . x)) 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x)))
.= (TRUE 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x))) by XBOOLEAN:102
.= TRUE '&' (('not' (a . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' b) 'imp' ('not' (a 'imp' ('not' b)))) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:35
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y
 for x being Element of Y holds (('not' (a 'imp' ('not' b))) 'imp' (a '&' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (('not' (a 'imp' ('not' b))) 'imp' (a '&' b)) . x = TRUE
(('not' (a 'imp' ('not' b))) 'imp' (a '&' b)) . x = ('not' (('not' (a 'imp' ('not' b))) . x)) 'or' ((a '&' b) . x) by BVFUNC_1:def_8
.= ('not' ('not' ((a 'imp' ('not' b)) . x))) 'or' ((a '&' b) . x) by MARGREL1:def_19
.= ('not' ('not' ((a 'imp' ('not' b)) . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (('not' b) . x)) 'or' ((a . x) '&' (b . x)) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19
.= ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (a . x)) '&' ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (b . x)) by XBOOLEAN:9
.= ((('not' (a . x)) 'or' (a . x)) 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x)))
.= (TRUE 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x))) by XBOOLEAN:102
.= TRUE '&' (('not' (a . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (('not' (a 'imp' ('not' b))) 'imp' (a '&' b)) . x = TRUE ; ::_thesis: verum
end;
hence  ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem Th36: :: BVFUNC_6:36
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) = I_el Y
 for x being Element of Y holds (('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE
(('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b))) . x = ('not' (('not' (a '&' b)) . x)) 'or' ((('not' a) 'or' ('not' b)) . x) by BVFUNC_1:def_8
.= ((a '&' b) . x) 'or' ((('not' a) 'or' ('not' b)) . x) by MARGREL1:def_19
.= ((a . x) '&' (b . x)) 'or' ((('not' a) 'or' ('not' b)) . x) by MARGREL1:def_20
.= ((('not' a) . x) 'or' (('not' b) . x)) 'or' ((a . x) '&' (b . x)) by BVFUNC_1:def_4
.= (('not' (a . x)) 'or' (('not' b) . x)) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19
.= ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (a . x)) '&' ((('not' (a . x)) 'or' ('not' (b . x))) 'or' (b . x)) by XBOOLEAN:9
.= ((('not' (a . x)) 'or' (a . x)) 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x)))
.= (TRUE 'or' ('not' (b . x))) '&' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x))) by XBOOLEAN:102
.= TRUE '&' (('not' (a . x)) 'or' TRUE) by XBOOLEAN:102
.= TRUE ;
hence  (('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b))) . x = TRUE ; ::_thesis: verum
end;
hence  ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:37
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (('not' a) 'or' ('not' b)) 'imp' ('not' (a '&' b)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (('not' a) 'or' ('not' b)) 'imp' ('not' (a '&' b)) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'or' ('not' b)) 'imp' ('not' (a '&' b)) = I_el Y
thus (('not' a) 'or' ('not' b)) 'imp' ('not' (a '&' b)) = ('not' (a '&' b)) 'imp' ('not' (a '&' b)) by BVFUNC_1:14
.= ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) by BVFUNC_1:14
.= I_el Y by Th36 ; ::_thesis: verum
end;

theorem :: BVFUNC_6:38
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' a = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' a = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' a = I_el Y
 for x being Element of Y holds ((a '&' b) 'imp' a) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' b) 'imp' a) . x = TRUE
((a '&' b) 'imp' a) . x = ('not' ((a '&' b) . x)) 'or' (a . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (a . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' (a . x)) 'or' ('not' (b . x))
.= TRUE 'or' ('not' (b . x)) by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' b) 'imp' a) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' b) 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' (a 'or' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' (a 'or' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' (a 'or' b) = I_el Y
 for x being Element of Y holds ((a '&' b) 'imp' (a 'or' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' b) 'imp' (a 'or' b)) . x = TRUE
((a '&' b) 'imp' (a 'or' b)) . x = ('not' ((a '&' b) . x)) 'or' ((a 'or' b) . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((a 'or' b) . x) by MARGREL1:def_20
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' ((a . x) 'or' (b . x)) by BVFUNC_1:def_4
.= (('not' (b . x)) 'or' (('not' (a . x)) 'or' (a . x))) 'or' (b . x)
.= (('not' (b . x)) 'or' TRUE) 'or' (b . x) by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' b) 'imp' (a 'or' b)) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' b) 'imp' (a 'or' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' b = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' b = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'imp' b = I_el Y
 for x being Element of Y holds ((a '&' b) 'imp' b) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a '&' b) 'imp' b) . x = TRUE
((a '&' b) 'imp' b) . x = ('not' ((a '&' b) . x)) 'or' (b . x) by BVFUNC_1:def_8
.= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (b . x) by MARGREL1:def_20
.= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (b . x))
.= ('not' (a . x)) 'or' TRUE by XBOOLEAN:102
.= TRUE ;
hence  ((a '&' b) 'imp' b) . x = TRUE ; ::_thesis: verum
end;
hence  (a '&' b) 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:41
for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (a '&' a) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' (a '&' a) = I_el Y
let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' (a '&' a) = I_el Y
 for x being Element of Y holds (a 'imp' (a '&' a)) . x = TRUE
proof
let x be Element of Y; ::_thesis: (a 'imp' (a '&' a)) . x = TRUE
(a 'imp' (a '&' a)) . x = TRUE '&' (('not' (a . x)) 'or' (a . x)) by BVFUNC_1:def_8
.= TRUE by XBOOLEAN:102 ;
hence  (a 'imp' (a '&' a)) . x = TRUE ; ::_thesis: verum
end;
hence  a 'imp' (a '&' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem Th42: :: BVFUNC_6:42
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y
 for x being Element of Y holds ((a 'eqv' b) 'imp' (a 'imp' b)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'eqv' b) 'imp' (a 'imp' b)) . x = TRUE
((a 'eqv' b) 'imp' (a 'imp' b)) . x = ('not' ((a 'eqv' b) . x)) 'or' ((a 'imp' b) . x) by BVFUNC_1:def_8
.= ((a . x) 'xor' (b . x)) 'or' ((a 'imp' b) . x) by BVFUNC_1:def_9
.= ((('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x)))) 'or' ('not' ((a . x) '&' ('not' (b . x)))) by BVFUNC_1:def_8
.= (('not' (a . x)) '&' (b . x)) 'or' (((a . x) '&' ('not' (b . x))) 'or' ('not' ((a . x) '&' ('not' (b . x)))))
.= (('not' (a . x)) '&' (b . x)) 'or' TRUE by XBOOLEAN:102
.= TRUE ;
hence  ((a 'eqv' b) 'imp' (a 'imp' b)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:43
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (b 'imp' a) = I_el Y by Th42;

theorem :: BVFUNC_6:44
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y
 for x being Element of Y holds (((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c))) . x = TRUE
(((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c))) . x = ('not' (((a 'or' b) 'or' c) . x)) 'or' ((a 'or' (b 'or' c)) . x) by BVFUNC_1:def_8
.= ('not' (((a 'or' b) . x) 'or' (c . x))) 'or' ((a 'or' (b 'or' c)) . x) by BVFUNC_1:def_4
.= ('not' (((a . x) 'or' (b . x)) 'or' (c . x))) 'or' ((a 'or' (b 'or' c)) . x) by BVFUNC_1:def_4
.= ('not' (((a . x) 'or' (b . x)) 'or' (c . x))) 'or' ((a . x) 'or' ((b 'or' c) . x)) by BVFUNC_1:def_4
.= ('not' (((a . x) 'or' (b . x)) 'or' (c . x))) 'or' ((a . x) 'or' ((b . x) 'or' (c . x))) by BVFUNC_1:def_4
.= TRUE by XBOOLEAN:102 ;
hence  (((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c))) . x = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:45
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y
 for x being Element of Y holds (((a '&' b) '&' c) 'imp' (a '&' (b '&' c))) . x = TRUE
proof
let x be Element of Y; ::_thesis: (((a '&' b) '&' c) 'imp' (a '&' (b '&' c))) . x = TRUE
(((a '&' b) '&' c) 'imp' (a '&' (b '&' c))) . x = ('not' (((a '&' b) '&' c) . x)) 'or' ((a '&' (b '&' c)) . x) by BVFUNC_1:def_8
.= ('not' (((a '&' b) . x) '&' (c . x))) 'or' ((a '&' (b '&' c)) . x) by MARGREL1:def_20
.= ('not' (((a . x) '&' (b . x)) '&' (c . x))) 'or' ((a '&' (b '&' c)) . x) by MARGREL1:def_20
.= ('not' (((a . x) '&' (b . x)) '&' (c . x))) 'or' ((a . x) '&' ((b '&' c) . x)) by MARGREL1:def_20
.= ('not' (((a . x) '&' (b . x)) '&' (c . x))) 'or' ((a . x) '&' ((b . x) '&' (c . x))) by MARGREL1:def_20
.= TRUE by XBOOLEAN:102 ;
hence  (((a '&' b) '&' c) 'imp' (a '&' (b '&' c))) . x = TRUE ; ::_thesis: verum
end;
hence  ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;

theorem :: BVFUNC_6:46
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y
 for x being Element of Y holds ((a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c)) . x = TRUE
proof
let x be Element of Y; ::_thesis: ((a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c)) . x = TRUE
((a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c)) . x = ('not' ((a 'or' (b 'or' c)) . x)) 'or' (((a 'or' b) 'or' c) . x) by BVFUNC_1:def_8
.= ('not' ((a . x) 'or' ((b 'or' c) . x))) 'or' (((a 'or' b) 'or' c) . x) by BVFUNC_1:def_4
.= ('not' ((a . x) 'or' ((b . x) 'or' (c . x)))) 'or' (((a 'or' b) 'or' c) . x) by BVFUNC_1:def_4
.= ('not' ((a . x) 'or' ((b . x) 'or' (c . x)))) 'or' (((a 'or' b) . x) 'or' (c . x)) by BVFUNC_1:def_4
.= ('not' ((a . x) 'or' ((b . x) 'or' (c . x)))) 'or' (((a . x) 'or' (b . x)) 'or' (c . x)) by BVFUNC_1:def_4
.= TRUE by XBOOLEAN:102 ;
hence  ((a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c)) . x = TRUE ; ::_thesis: verum
end;
hence  (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum
end;