:: 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;