:: BVFUNC_5 semantic presentation begin theorem :: BVFUNC_5:1 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y ) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y ) let a, b be Function of Y,BOOLEAN; ::_thesis: ( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y ) now__::_thesis:_(_a_'&'_b_=_I_el_Y_implies_(_a_=_I_el_Y_&_b_=_I_el_Y_)_) assume A1: a '&' b = I_el Y ; ::_thesis: ( a = I_el Y & b = I_el Y ) percases ( ( a = I_el Y & b = I_el Y ) or ( a = I_el Y & b <> I_el Y ) or ( a <> I_el Y & b = I_el Y ) or ( a <> I_el Y & b <> I_el Y ) ) ; suppose ( a = I_el Y & b = I_el Y ) ; ::_thesis: ( a = I_el Y & b = I_el Y ) hence ( a = I_el Y & b = I_el Y ) ; ::_thesis: verum end; suppose ( a = I_el Y & b <> I_el Y ) ; ::_thesis: ( a = I_el Y & b = I_el Y ) hence ( a = I_el Y & b = I_el Y ) by A1, BVFUNC_1:6; ::_thesis: verum end; suppose ( a <> I_el Y & b = I_el Y ) ; ::_thesis: ( a = I_el Y & b = I_el Y ) hence ( a = I_el Y & b = I_el Y ) by A1, BVFUNC_1:6; ::_thesis: verum end; supposeA2: ( a <> I_el Y & b <> I_el Y ) ; ::_thesis: ( a = I_el Y & b = I_el Y ) for x being Element of Y holds a . x = TRUE proof let x be Element of Y; ::_thesis: a . x = TRUE (a '&' b) . x = TRUE by A1, BVFUNC_1:def_11; then (a . x) '&' (b . x) = TRUE by MARGREL1:def_20; hence a . x = TRUE by MARGREL1:12; ::_thesis: verum end; hence ( a = I_el Y & b = I_el Y ) by A2, BVFUNC_1:def_11; ::_thesis: verum end; end; end; hence ( ( a = I_el Y & b = I_el Y ) iff a '&' b = I_el Y ) ; ::_thesis: verum end; theorem Th2: :: BVFUNC_5:2 for Y being non empty set for b being Function of Y,BOOLEAN st (I_el Y) 'imp' b = I_el Y holds b = I_el Y proof let Y be non empty set ; ::_thesis: for b being Function of Y,BOOLEAN st (I_el Y) 'imp' b = I_el Y holds b = I_el Y set a = I_el Y; let b be Function of Y,BOOLEAN; ::_thesis: ( (I_el Y) 'imp' b = I_el Y implies b = I_el Y ) assume A1: (I_el Y) 'imp' b = 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 ((I_el Y) 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11; then ( (I_el Y) . x = TRUE & ('not' ((I_el Y) . x)) 'or' (b . x) = TRUE ) by BVFUNC_1:def_8, BVFUNC_1:def_11; then FALSE 'or' (b . x) = TRUE by MARGREL1:11; hence b . x = TRUE by BINARITH:3; ::_thesis: verum end; hence b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:3 for Y being non empty set for a, b being Function of Y,BOOLEAN st a = 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 = I_el Y holds a 'or' b = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( a = I_el Y implies a 'or' b = I_el Y ) assume A1: a = 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 . x = TRUE by A1, BVFUNC_1:def_11; then (a 'or' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_4 .= TRUE by BINARITH:10 ; 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_5:4 for Y being non empty set for a, b being Function of Y,BOOLEAN st b = 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 b = I_el Y holds a 'imp' b = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( b = I_el Y implies a 'imp' b = I_el Y ) assume A1: b = 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 b . x = TRUE by A1, BVFUNC_1:def_11; then (a 'imp' b) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8 .= TRUE by BINARITH:10 ; hence (a 'imp' b) . x = TRUE ; ::_thesis: verum end; hence a 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:5 for Y being non empty set for a, b being Function of Y,BOOLEAN st '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 'not' a = I_el Y holds a 'imp' b = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( 'not' a = I_el Y implies a 'imp' b = I_el Y ) assume A1: '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 ('not' a) . x = TRUE by A1, BVFUNC_1:def_11; then 'not' (a . x) = TRUE by MARGREL1:def_19; then (a 'imp' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_8 .= TRUE by BINARITH:10 ; hence (a 'imp' b) . x = TRUE ; ::_thesis: verum end; hence a 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:6 for Y being non empty set for a being Function of Y,BOOLEAN holds 'not' (a '&' ('not' a)) = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds 'not' (a '&' ('not' a)) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: 'not' (a '&' ('not' a)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ('not' (a '&' ('not' a))) . x = (I_el Y) . x thus ('not' (a '&' ('not' a))) . x = 'not' ((a '&' ('not' a)) . x) by MARGREL1:def_19 .= 'not' ((a . x) '&' (('not' a) . x)) by MARGREL1:def_20 .= 'not' ((a . x) '&' ('not' (a . x))) by MARGREL1:def_19 .= TRUE by XBOOLEAN:102 .= (I_el Y) . x by BVFUNC_1:def_11 ; ::_thesis: verum end; theorem :: BVFUNC_5:7 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'imp' a = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'imp' a = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' a) . x = (I_el Y) . x A5: ( (a 'imp' a) . x = ('not' (a . x)) 'or' (a . x) & (I_el Y) . x = TRUE ) by BVFUNC_1:def_8, BVFUNC_1:def_11; A6: 'not' FALSE = TRUE by MARGREL1:11; now__::_thesis:_(_(_a_._x_=_TRUE_&_(a_'imp'_a)_._x_=_(I_el_Y)_._x_)_or_(_a_._x_=_FALSE_&_(a_'imp'_a)_._x_=_(I_el_Y)_._x_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: (a 'imp' a) . x = (I_el Y) . x hence (a 'imp' a) . x = (I_el Y) . x by A5, BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: (a 'imp' a) . x = (I_el Y) . x hence (a 'imp' a) . x = (I_el Y) . x by A6, A5, BINARITH:10; ::_thesis: verum end; end; end; hence (a 'imp' a) . x = (I_el Y) . x ; ::_thesis: verum end; theorem :: BVFUNC_5:8 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ( a 'imp' b = I_el Y iff ('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 = I_el Y iff ('not' b) 'imp' ('not' a) = I_el Y ) let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y iff ('not' b) 'imp' ('not' a) = I_el Y ) A1: now__::_thesis:_(_('not'_b)_'imp'_('not'_a)_=_I_el_Y_implies_a_'imp'_b_=_I_el_Y_) assume A2: ('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 (('not' b) 'imp' ('not' a)) . x = TRUE by A2, BVFUNC_1:def_11; then ('not' (('not' b) . x)) 'or' (('not' a) . x) = TRUE by BVFUNC_1:def_8; then ('not' ('not' (b . x))) 'or' (('not' a) . x) = TRUE by MARGREL1:def_19; then A3: ('not' ('not' (b . x))) 'or' ('not' (a . x)) = TRUE by MARGREL1:def_19; A4: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_(a_'imp'_b)_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_(a_'imp'_b)_._x_=_TRUE_)_) percases ( 'not' (a . x) = TRUE or b . x = TRUE ) by A3, A4, BINARITH:3; case 'not' (a . x) = TRUE ; ::_thesis: (a 'imp' b) . x = TRUE then (a 'imp' b) . x = TRUE 'or' (b . x) by BVFUNC_1:def_8 .= TRUE by BINARITH:10 ; hence (a 'imp' b) . x = TRUE ; ::_thesis: verum end; case b . x = TRUE ; ::_thesis: (a 'imp' b) . x = TRUE then (a 'imp' b) . x = ('not' (a . x)) 'or' TRUE by BVFUNC_1:def_8 .= TRUE by BINARITH:10 ; hence (a 'imp' b) . x = TRUE ; ::_thesis: verum end; end; end; hence (a 'imp' b) . x = TRUE ; ::_thesis: verum end; hence a 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; now__::_thesis:_(_a_'imp'_b_=_I_el_Y_implies_('not'_b)_'imp'_('not'_a)_=_I_el_Y_) assume A5: a 'imp' b = I_el Y ; ::_thesis: ('not' b) 'imp' ('not' a) = I_el Y for x being Element of Y holds (('not' b) 'imp' ('not' a)) . x = TRUE proof let x be Element of Y; ::_thesis: (('not' b) 'imp' ('not' a)) . x = TRUE (a 'imp' b) . x = TRUE by A5, BVFUNC_1:def_11; then A6: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8; A7: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_(('not'_b)_'imp'_('not'_a))_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_(('not'_b)_'imp'_('not'_a))_._x_=_TRUE_)_) percases ( 'not' (a . x) = TRUE or b . x = TRUE ) by A6, A7, BINARITH:3; caseA8: 'not' (a . x) = TRUE ; ::_thesis: (('not' b) 'imp' ('not' a)) . x = TRUE (('not' b) 'imp' ('not' a)) . x = ('not' (('not' b) . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8 .= ('not' (('not' b) . x)) 'or' TRUE by A8, MARGREL1:def_19 .= TRUE by BINARITH:10 ; hence (('not' b) 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum end; caseA9: b . x = TRUE ; ::_thesis: (('not' b) 'imp' ('not' a)) . x = TRUE ('not' b) . x = 'not' (b . x) by MARGREL1:def_19; then (('not' b) 'imp' ('not' a)) . x = ('not' ('not' (b . x))) 'or' (('not' a) . x) by BVFUNC_1:def_8 .= TRUE by A9, BINARITH:10 ; hence (('not' b) 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum end; end; end; hence (('not' b) 'imp' ('not' a)) . x = TRUE ; ::_thesis: verum end; hence ('not' b) 'imp' ('not' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; hence ( a 'imp' b = I_el Y iff ('not' b) 'imp' ('not' a) = I_el Y ) by A1; ::_thesis: verum end; theorem :: BVFUNC_5:9 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y & b 'imp' c = I_el Y holds a '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' b = I_el Y & b 'imp' c = I_el Y holds a 'imp' c = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y & b 'imp' c = I_el Y implies a 'imp' c = I_el Y ) assume that A1: a 'imp' b = I_el Y and A2: b 'imp' c = I_el Y ; ::_thesis: a 'imp' c = I_el Y for x being Element of Y holds (a 'imp' c) . x = TRUE proof let x be Element of Y; ::_thesis: (a 'imp' c) . x = TRUE A3: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3; A4: (a 'imp' c) . x = ('not' (a . x)) 'or' (c . x) by BVFUNC_1:def_8; (b 'imp' c) . x = TRUE by A2, BVFUNC_1:def_11; then A5: ('not' (b . x)) 'or' (c . x) = TRUE by BVFUNC_1:def_8; (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11; then A6: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8; A7: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_'not'_(b_._x)_=_TRUE_&_(a_'imp'_c)_._x_=_TRUE_)_or_(_'not'_(a_._x)_=_TRUE_&_c_._x_=_TRUE_&_(a_'imp'_c)_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_'not'_(b_._x)_=_TRUE_&_(a_'imp'_c)_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_c_._x_=_TRUE_&_(a_'imp'_c)_._x_=_TRUE_)_) percases ( ( 'not' (a . x) = TRUE & 'not' (b . x) = TRUE ) or ( 'not' (a . x) = TRUE & c . x = TRUE ) or ( b . x = TRUE & 'not' (b . x) = TRUE ) or ( b . x = TRUE & c . x = TRUE ) ) by A6, A7, A5, A3, BINARITH:3; case ( 'not' (a . x) = TRUE & 'not' (b . x) = TRUE ) ; ::_thesis: (a 'imp' c) . x = TRUE hence (a 'imp' c) . x = TRUE by A4, BINARITH:10; ::_thesis: verum end; case ( 'not' (a . x) = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' c) . x = TRUE hence (a 'imp' c) . x = TRUE by A4; ::_thesis: verum end; case ( b . x = TRUE & 'not' (b . x) = TRUE ) ; ::_thesis: (a 'imp' c) . x = TRUE hence (a 'imp' c) . x = TRUE by MARGREL1:11; ::_thesis: verum end; case ( b . x = TRUE & c . x = TRUE ) ; ::_thesis: (a 'imp' c) . x = TRUE hence (a 'imp' c) . x = TRUE by A4, BINARITH:10; ::_thesis: verum end; end; end; hence (a 'imp' c) . x = TRUE ; ::_thesis: verum end; hence a 'imp' c = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:10 for Y being non empty set for a, b being Function of Y,BOOLEAN st a 'imp' b = I_el Y & a 'imp' ('not' b) = I_el Y holds 'not' a = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a 'imp' b = I_el Y & a 'imp' ('not' b) = I_el Y holds 'not' a = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y & a 'imp' ('not' b) = I_el Y implies 'not' a = I_el Y ) assume that A1: a 'imp' b = I_el Y and A2: a 'imp' ('not' b) = I_el Y ; ::_thesis: 'not' a = I_el Y for x being Element of Y holds ('not' a) . x = TRUE proof let x be Element of Y; ::_thesis: ('not' a) . 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; (a 'imp' ('not' b)) . x = TRUE by A2, BVFUNC_1:def_11; then A4: ('not' (a . x)) 'or' (('not' b) . x) = TRUE by BVFUNC_1:def_8; A5: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_'not'_(a_._x)_=_TRUE_&_('not'_a)_._x_=_TRUE_)_or_(_'not'_(a_._x)_=_TRUE_&_('not'_b)_._x_=_TRUE_&_('not'_a)_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_'not'_(a_._x)_=_TRUE_&_('not'_a)_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_('not'_b)_._x_=_TRUE_&_('not'_a)_._x_=_TRUE_)_) percases ( ( 'not' (a . x) = TRUE & 'not' (a . x) = TRUE ) or ( 'not' (a . x) = TRUE & ('not' b) . x = TRUE ) or ( b . x = TRUE & 'not' (a . x) = TRUE ) or ( b . x = TRUE & ('not' b) . x = TRUE ) ) by A3, A5, A4, BINARITH:3; case ( 'not' (a . x) = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: ('not' a) . x = TRUE hence ('not' a) . x = TRUE by MARGREL1:def_19; ::_thesis: verum end; case ( 'not' (a . x) = TRUE & ('not' b) . x = TRUE ) ; ::_thesis: ('not' a) . x = TRUE hence ('not' a) . x = TRUE by MARGREL1:def_19; ::_thesis: verum end; case ( b . x = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: ('not' a) . x = TRUE hence ('not' a) . x = TRUE by MARGREL1:def_19; ::_thesis: verum end; caseA6: ( b . x = TRUE & ('not' b) . x = TRUE ) ; ::_thesis: ('not' a) . x = TRUE then 'not' (b . x) = TRUE by MARGREL1:def_19; hence ('not' a) . x = TRUE by A6, MARGREL1:11; ::_thesis: verum end; end; end; hence ('not' a) . x = TRUE ; ::_thesis: verum end; hence 'not' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:11 for Y being non empty set for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'imp' a = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'imp' a = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'imp' a) 'imp' a = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x A5: 'not' (('not' (('not' a) . x)) 'or' (a . x)) = 'not' ((a . x) 'or' (a . x)) by MARGREL1:def_19 .= 'not' (a . x) ; A6: ((('not' a) 'imp' a) 'imp' a) . x = ('not' ((('not' a) 'imp' a) . x)) 'or' (a . x) by BVFUNC_1:def_8 .= ('not' (a . x)) 'or' (a . x) by A5, BVFUNC_1:def_8 ; A7: (I_el Y) . x = TRUE by BVFUNC_1:def_11; now__::_thesis:_(_(_a_._x_=_TRUE_&_((('not'_a)_'imp'_a)_'imp'_a)_._x_=_(I_el_Y)_._x_)_or_(_a_._x_=_FALSE_&_((('not'_a)_'imp'_a)_'imp'_a)_._x_=_(I_el_Y)_._x_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x hence ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x by A6, A7, BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x then ((('not' a) 'imp' a) 'imp' a) . x = TRUE 'or' FALSE by A6, MARGREL1:11 .= TRUE by BINARITH:10 ; hence ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; end; end; hence ((('not' a) 'imp' a) 'imp' a) . x = (I_el Y) . x ; ::_thesis: verum end; theorem :: BVFUNC_5:12 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' 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' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c))) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x = (I_el Y) . x A5: ((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x = ('not' ((a 'imp' b) . x)) 'or' ((('not' (b '&' c)) 'imp' ('not' (a '&' c))) . x) by BVFUNC_1:def_8 .= ('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x)) by BVFUNC_1:def_8 ; A6: ('not' (a '&' c)) . x = (('not' a) 'or' ('not' c)) . x by BVFUNC_1:14 .= (('not' a) . x) 'or' (('not' c) . x) by BVFUNC_1:def_4 .= ('not' (a . x)) 'or' (('not' c) . x) by MARGREL1:def_19 .= ('not' (a . x)) 'or' ('not' (c . x)) by MARGREL1:def_19 ; now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; then ('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x)) = TRUE by BINARITH:10; then A7: ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' (('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x))) = (('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x) by MARGREL1:14; A8: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A9: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; 'not' (('not' (b '&' c)) . x) = 'not' ('not' ((b '&' c) . x)) by MARGREL1:def_19 .= (b . x) '&' (c . x) by MARGREL1:def_20 ; then A10: ('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x) = ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (c . x)) by A6, XBOOLEAN:9 .= ((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) '&' (('not' (a . x)) 'or' (('not' (c . x)) 'or' (c . x))) by BINARITH:11 ; 'not' ((a 'imp' b) . x) = 'not' (('not' (a . x)) 'or' (b . x)) by BVFUNC_1:def_8 .= (a . x) '&' ('not' (b . x)) ; then ('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x)) = (((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' (((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' ('not' (b . x))) by A10, A7, XBOOLEAN:9 .= (((('not' (a . x)) 'or' ('not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x)))) by BINARITH:11 .= (((('not' (c . x)) 'or' ('not' (a . x))) 'or' (a . x)) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x)))) by BINARITH:11 .= ((('not' (c . x)) 'or' (('not' (a . x)) 'or' (a . x))) 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' ((b . x) 'or' ('not' (b . x)))) by BINARITH:11 ; then ('not' ((a 'imp' b) . x)) 'or' (('not' (('not' (b '&' c)) . x)) 'or' (('not' (a '&' c)) . x)) = (TRUE 'or' (b . x)) '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' TRUE) by A8, A9, BINARITH:10 .= TRUE '&' ((('not' (a . x)) 'or' ('not' (c . x))) 'or' TRUE) by BINARITH:10 .= TRUE '&' TRUE by BINARITH:10 .= TRUE ; hence ((a 'imp' b) 'imp' (('not' (b '&' c)) 'imp' ('not' (a '&' c)))) . x = (I_el Y) . x by A5, BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:13 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))) . x = (I_el Y) . x A5: ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))) . x = ('not' ((a 'imp' b) . x)) 'or' (((b 'imp' c) 'imp' (a 'imp' c)) . x) by BVFUNC_1:def_8 .= ('not' ((a 'imp' b) . x)) 'or' (('not' ((b 'imp' c) . x)) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 ; A6: 'not' ((b 'imp' c) . x) = 'not' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8 .= (b . x) '&' ('not' (c . x)) ; A7: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A8: (a 'imp' c) . x = ('not' (a . x)) 'or' (c . x) by BVFUNC_1:def_8; A9: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; A10: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; 'not' ((a 'imp' b) . x) = 'not' (('not' (a . x)) 'or' (b . x)) by BVFUNC_1:def_8 .= (a . x) '&' ('not' (b . x)) ; then ('not' ((a 'imp' b) . x)) 'or' (('not' ((b 'imp' c) . x)) 'or' ((a 'imp' c) . x)) = ((((b . x) '&' ('not' (c . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (a . x)) '&' ((((b . x) '&' ('not' (c . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (b . x))) by A6, A8, XBOOLEAN:9 .= (((b . x) '&' ('not' (c . x))) 'or' (((c . x) 'or' ('not' (a . x))) 'or' (a . x))) '&' ((((b . x) '&' ('not' (c . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (b . x))) by BINARITH:11 .= (((b . x) '&' ('not' (c . x))) 'or' ((c . x) 'or' (('not' (a . x)) 'or' (a . x)))) '&' (((('not' (a . x)) 'or' (c . x)) 'or' ((b . x) '&' ('not' (c . x)))) 'or' ('not' (b . x))) by BINARITH:11 .= (((b . x) '&' ('not' (c . x))) 'or' ((c . x) 'or' (('not' (a . x)) 'or' (a . x)))) '&' ((('not' (a . x)) 'or' (c . x)) 'or' ((('not' (c . x)) '&' (b . x)) 'or' ('not' (b . x)))) by BINARITH:11 .= (((b . x) '&' ('not' (c . x))) 'or' ((c . x) 'or' (('not' (a . x)) 'or' (a . x)))) '&' ((('not' (a . x)) 'or' (c . x)) 'or' ((('not' (b . x)) 'or' ('not' (c . x))) '&' (('not' (b . x)) 'or' (b . x)))) by XBOOLEAN:9 .= (((b . x) '&' ('not' (c . x))) 'or' TRUE) '&' ((('not' (a . x)) 'or' (c . x)) 'or' ((('not' (b . x)) 'or' ('not' (c . x))) '&' TRUE)) by A7, A10, BINARITH:10 .= TRUE '&' ((('not' (a . x)) 'or' (c . x)) 'or' ((('not' (b . x)) 'or' ('not' (c . x))) '&' TRUE)) by BINARITH:10 .= (('not' (a . x)) 'or' (c . x)) 'or' (TRUE '&' (('not' (b . x)) 'or' ('not' (c . x)))) by MARGREL1:14 .= (('not' (a . x)) 'or' (c . x)) 'or' (('not' (c . x)) 'or' ('not' (b . x))) by MARGREL1:14 .= ((('not' (a . x)) 'or' (c . x)) 'or' ('not' (c . x))) 'or' ('not' (b . x)) by BINARITH:11 .= (('not' (a . x)) 'or' TRUE) 'or' ('not' (b . x)) by A9, BINARITH:11 .= TRUE 'or' ('not' (b . x)) by BINARITH:10 .= TRUE by BINARITH:10 ; hence ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))) . x = (I_el Y) . x by A5, BVFUNC_1:def_11; ::_thesis: verum end; theorem Th14: :: BVFUNC_5:14 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds (b 'imp' c) 'imp' (a 'imp' c) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds (b 'imp' c) 'imp' (a 'imp' c) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' b = I_el Y implies (b 'imp' c) 'imp' (a 'imp' c) = I_el Y ) assume A1: a 'imp' b = I_el Y ; ::_thesis: (b 'imp' c) 'imp' (a 'imp' c) = I_el Y for x being Element of Y holds ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE proof let x be Element of Y; ::_thesis: ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE A2: ((b 'imp' c) 'imp' (a 'imp' c)) . x = ('not' ((b 'imp' c) . x)) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (('not' (b . x)) 'or' (c . x))) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_8 .= (('not' (a . x)) 'or' (c . x)) 'or' ((b . x) '&' ('not' (c . x))) by BVFUNC_1:def_8 ; A3: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; (a 'imp' b) . x = TRUE by A1, BVFUNC_1:def_11; then A4: ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8; A5: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_((b_'imp'_c)_'imp'_(a_'imp'_c))_._x_=_TRUE_)_or_(_b_._x_=_TRUE_&_((b_'imp'_c)_'imp'_(a_'imp'_c))_._x_=_TRUE_)_) percases ( 'not' (a . x) = TRUE or b . x = TRUE ) by A4, A5, BINARITH:3; case 'not' (a . x) = TRUE ; ::_thesis: ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE then ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE 'or' ((b . x) '&' ('not' (c . x))) by A2, BINARITH:10 .= TRUE by BINARITH:10 ; hence ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE ; ::_thesis: verum end; case b . x = TRUE ; ::_thesis: ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE then ((b 'imp' c) 'imp' (a 'imp' c)) . x = (('not' (a . x)) 'or' (c . x)) 'or' ('not' (c . x)) by A2, MARGREL1:14 .= ('not' (a . x)) 'or' TRUE by A3, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE ; ::_thesis: verum end; end; end; hence ((b 'imp' c) 'imp' (a 'imp' c)) . x = TRUE ; ::_thesis: verum end; hence (b 'imp' c) 'imp' (a 'imp' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem Th15: :: BVFUNC_5:15 for Y being non empty set for a, b being Function of Y,BOOLEAN holds 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 b 'imp' (a 'imp' b) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: b 'imp' (a 'imp' b) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (b 'imp' (a 'imp' b)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; (b 'imp' (a 'imp' b)) . x = ('not' (b . x)) 'or' ((a 'imp' b) . x) by BVFUNC_1:def_8 .= ('not' (b . x)) 'or' ((b . x) 'or' ('not' (a . x))) by BVFUNC_1:def_8 .= TRUE 'or' ('not' (a . x)) by A5, BINARITH:11 .= TRUE by BINARITH:10 ; hence (b 'imp' (a 'imp' b)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:16 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c) '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 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y b 'imp' (a 'imp' b) = I_el Y by Th15; hence ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y by Th14; ::_thesis: verum end; theorem :: BVFUNC_5:17 for Y being non empty set for a, b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds b 'imp' ((b 'imp' a) 'imp' a) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: b 'imp' ((b 'imp' a) 'imp' a) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (b 'imp' ((b 'imp' a) 'imp' a)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; (b 'imp' ((b 'imp' a) 'imp' a)) . x = ('not' (b . x)) 'or' (((b 'imp' a) 'imp' a) . x) by BVFUNC_1:def_8 .= ('not' (b . x)) 'or' (('not' ((b 'imp' a) . x)) 'or' (a . x)) by BVFUNC_1:def_8 .= ('not' (b . x)) 'or' (('not' (('not' (b . x)) 'or' (a . x))) 'or' (a . x)) by BVFUNC_1:def_8 .= ('not' (b . x)) 'or' (((a . x) 'or' (b . x)) '&' TRUE) by A6, XBOOLEAN:9 .= ('not' (b . x)) 'or' ((a . x) 'or' (b . x)) by MARGREL1:14 .= (('not' (b . x)) 'or' (b . x)) 'or' (a . x) by BINARITH:11 .= TRUE by A5, BINARITH:10 ; hence (b 'imp' ((b 'imp' a) 'imp' a)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:18 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))) . x = (I_el Y) . x A5: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A7: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; ((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))) . x = ('not' ((c 'imp' (b 'imp' a)) . x)) 'or' ((b 'imp' (c 'imp' a)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (c . x)) 'or' ((b 'imp' a) . x))) 'or' ((b 'imp' (c 'imp' a)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (c . x)) 'or' (('not' (b . x)) 'or' (a . x)))) 'or' ((b 'imp' (c 'imp' a)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (c . x)) 'or' (('not' (b . x)) 'or' (a . x)))) 'or' (('not' (b . x)) 'or' ((c 'imp' a) . x)) by BVFUNC_1:def_8 .= ((c . x) '&' (('not' ('not' (b . x))) '&' ('not' (a . x)))) 'or' (('not' (b . x)) 'or' (('not' (c . x)) 'or' (a . x))) by BVFUNC_1:def_8 .= ((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' ((b . x) '&' ((c . x) '&' ('not' (a . x)))) by MARGREL1:16 .= (((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' (b . x)) '&' (((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' ((c . x) '&' ('not' (a . x)))) by XBOOLEAN:9 .= ((('not' (c . x)) 'or' (a . x)) 'or' TRUE) '&' (((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' ((c . x) '&' ('not' (a . x)))) by A5, BINARITH:11 .= TRUE '&' (((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' ((c . x) '&' ('not' (a . x)))) by BINARITH:10 .= ((('not' (c . x)) 'or' (a . x)) 'or' ('not' (b . x))) 'or' ((c . x) '&' ('not' (a . x))) by MARGREL1:14 .= (((a . x) 'or' ('not' (b . x))) 'or' ('not' (c . x))) 'or' ((c . x) '&' ('not' (a . x))) by BINARITH:11 .= ((a . x) 'or' ('not' (b . x))) 'or' (('not' (c . x)) 'or' ((c . x) '&' ('not' (a . x)))) by BINARITH:11 .= ((a . x) 'or' ('not' (b . x))) 'or' (TRUE '&' (('not' (c . x)) 'or' ('not' (a . x)))) by A7, XBOOLEAN:9 .= (('not' (b . x)) 'or' (a . x)) 'or' (('not' (c . x)) 'or' ('not' (a . x))) by MARGREL1:14 .= ((('not' (b . x)) 'or' (a . x)) 'or' ('not' (a . x))) 'or' ('not' (c . x)) by BINARITH:11 .= (('not' (b . x)) 'or' TRUE) 'or' ('not' (c . x)) by A6, BINARITH:11 .= TRUE 'or' ('not' (c . x)) by BINARITH:10 .= TRUE by BINARITH:10 ; hence ((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:19 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A7: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; ((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = ('not' ((b 'imp' c) . x)) 'or' (((a 'imp' b) 'imp' (a 'imp' c)) . x) by BVFUNC_1:def_8 .= ('not' ((b 'imp' c) . x)) 'or' (('not' ((a 'imp' b) . x)) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 .= ('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' ((a 'imp' b) . x)) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 .= ('not' (('not' (b . x)) 'or' (c . x))) 'or' (('not' (('not' (a . x)) 'or' (b . x))) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 .= ((b . x) '&' ('not' (c . x))) 'or' ((('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) by BVFUNC_1:def_8 .= ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' ('not' (c . x))) '&' ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x)) by XBOOLEAN:9 .= (((a . x) '&' ('not' (b . x))) 'or' ((('not' (a . x)) 'or' (c . x)) 'or' ('not' (c . x)))) '&' ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x)) by BINARITH:11 .= (((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' TRUE)) '&' ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x)) by A7, BINARITH:11 .= (((a . x) '&' ('not' (b . x))) 'or' TRUE) '&' ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x)) by BINARITH:10 .= TRUE '&' ((((a . x) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x)) by BINARITH:10 .= ((('not' (b . x)) '&' (a . x)) 'or' (('not' (a . x)) 'or' (c . x))) 'or' (b . x) by MARGREL1:14 .= (((('not' (a . x)) 'or' (c . x)) 'or' ('not' (b . x))) '&' ((('not' (a . x)) 'or' (c . x)) 'or' (a . x))) 'or' (b . x) by XBOOLEAN:9 .= (((('not' (a . x)) 'or' (c . x)) 'or' ('not' (b . x))) '&' ((c . x) 'or' (('not' (a . x)) 'or' (a . x)))) 'or' (b . x) by BINARITH:11 .= (((('not' (a . x)) 'or' (c . x)) 'or' ('not' (b . x))) '&' TRUE) 'or' (b . x) by A5, BINARITH:10 .= ((('not' (a . x)) 'or' (c . x)) 'or' ('not' (b . x))) 'or' (b . x) by MARGREL1:14 .= (('not' (a . x)) 'or' (c . x)) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:20 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (b 'imp' (b 'imp' c)) '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 (b 'imp' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (b 'imp' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; ((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)) . x = ('not' ((b 'imp' (b 'imp' c)) . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (('not' (b . x)) 'or' ((b 'imp' c) . x))) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (('not' (b . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8 .= ((b . x) '&' (('not' ('not' (b . x))) '&' ('not' (c . x)))) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8 .= (((b . x) '&' (b . x)) '&' ('not' (c . x))) 'or' (('not' (b . x)) 'or' (c . x)) by MARGREL1:16 .= (((c . x) 'or' ('not' (b . x))) 'or' (b . x)) '&' ((('not' (b . x)) 'or' (c . x)) 'or' ('not' (c . x))) by XBOOLEAN:9 .= ((c . x) 'or' TRUE) '&' ((('not' (b . x)) 'or' (c . x)) 'or' ('not' (c . x))) by A5, BINARITH:11 .= TRUE '&' ((('not' (b . x)) 'or' (c . x)) 'or' ('not' (c . x))) by BINARITH:10 .= (('not' (b . x)) 'or' (c . x)) 'or' ('not' (c . x)) by MARGREL1:14 .= ('not' (b . x)) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem Th21: :: BVFUNC_5:21 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_c_._x_=_TRUE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_or_(_c_._x_=_FALSE_&_('not'_(c_._x))_'or'_(c_._x)_=_TRUE_)_) percases ( c . x = TRUE or c . x = FALSE ) by XBOOLEAN:def_3; case c . x = TRUE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE hence ('not' (c . x)) 'or' (c . x) = TRUE by BINARITH:10; ::_thesis: verum end; case c . x = FALSE ; ::_thesis: ('not' (c . x)) 'or' (c . x) = TRUE then ('not' (c . x)) 'or' (c . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (c . x)) 'or' (c . x) = TRUE ; ::_thesis: verum end; end; end; A7: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; ((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = ('not' ((a 'imp' (b 'imp' c)) . x)) 'or' (((a 'imp' b) 'imp' (a 'imp' c)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' ((b 'imp' c) . x))) 'or' (((a 'imp' b) 'imp' (a 'imp' c)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' (((a 'imp' b) 'imp' (a 'imp' c)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' ((a 'imp' b) . x)) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)))) 'or' (('not' (('not' (a . x)) 'or' (b . x))) 'or' ((a 'imp' c) . x)) by BVFUNC_1:def_8 .= (('not' ('not' (a . x))) '&' (('not' ('not' (b . x))) '&' ('not' (c . x)))) 'or' ((('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x))) by BVFUNC_1:def_8 .= ((a . x) '&' ((b . x) '&' ('not' (c . x)))) 'or' ((((c . x) 'or' ('not' (a . x))) 'or' (a . x)) '&' (((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x)))) by XBOOLEAN:9 .= ((a . x) '&' ((b . x) '&' ('not' (c . x)))) 'or' (((c . x) 'or' TRUE) '&' (((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x)))) by A5, BINARITH:11 .= ((a . x) '&' ((b . x) '&' ('not' (c . x)))) 'or' (TRUE '&' (((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x)))) by BINARITH:10 .= (((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((a . x) '&' ((b . x) '&' ('not' (c . x)))) by MARGREL1:14 .= ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' (a . x)) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x)))) by XBOOLEAN:9 .= ((((c . x) 'or' ('not' (a . x))) 'or' (a . x)) 'or' ('not' (b . x))) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x)))) by BINARITH:11 .= (((c . x) 'or' TRUE) 'or' ('not' (b . x))) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x)))) by A5, BINARITH:11 .= (TRUE 'or' ('not' (b . x))) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x)))) by BINARITH:10 .= TRUE '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x)))) by BINARITH:10 .= (((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ((b . x) '&' ('not' (c . x))) by MARGREL1:14 .= ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' (b . x)) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ('not' (c . x))) by XBOOLEAN:9 .= (((c . x) 'or' ('not' (a . x))) 'or' TRUE) '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ('not' (c . x))) by A7, BINARITH:11 .= TRUE '&' ((((c . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) 'or' ('not' (c . x))) by BINARITH:10 .= (('not' (b . x)) 'or' ((c . x) 'or' ('not' (a . x)))) 'or' ('not' (c . x)) by MARGREL1:14 .= ((('not' (b . x)) 'or' ('not' (a . x))) 'or' (c . x)) 'or' ('not' (c . x)) by BINARITH:11 .= (('not' (b . x)) 'or' ('not' (a . x))) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:22 for Y being non empty set for a, b being Function of Y,BOOLEAN st a = I_el Y holds (a 'imp' b) 'imp' b = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a = I_el Y holds (a 'imp' b) 'imp' b = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( a = I_el Y implies (a 'imp' b) 'imp' b = I_el Y ) assume A1: a = I_el Y ; ::_thesis: (a 'imp' b) 'imp' b = I_el Y for x being Element of Y holds ((a 'imp' b) 'imp' b) . x = TRUE proof let x be Element of Y; ::_thesis: ((a 'imp' b) 'imp' b) . x = TRUE A2: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; A3: a . x = TRUE by A1, BVFUNC_1:def_11; ((a 'imp' b) 'imp' b) . x = ('not' ((a 'imp' b) . x)) 'or' (b . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (b . x))) 'or' (b . x) by BVFUNC_1:def_8 .= ((b . x) 'or' TRUE) '&' TRUE by A3, A2, XBOOLEAN:9 .= (b . x) 'or' TRUE by MARGREL1:14 .= TRUE by BINARITH:10 ; hence ((a 'imp' b) 'imp' b) . x = TRUE ; ::_thesis: verum end; hence (a 'imp' b) 'imp' b = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:23 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y holds b 'imp' (c 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y holds b 'imp' (c 'imp' a) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( c 'imp' (b 'imp' a) = I_el Y implies b 'imp' (c 'imp' a) = I_el Y ) assume A1: c 'imp' (b 'imp' a) = I_el Y ; ::_thesis: b 'imp' (c 'imp' a) = I_el Y for x being Element of Y holds (b 'imp' (c 'imp' a)) . x = TRUE proof let x be Element of Y; ::_thesis: (b 'imp' (c 'imp' a)) . x = TRUE (c 'imp' (b 'imp' a)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (c . x)) 'or' ((b 'imp' a) . x) = TRUE by BVFUNC_1:def_8; then A2: ('not' (c . x)) 'or' (('not' (b . x)) 'or' (a . x)) = TRUE by BVFUNC_1:def_8; (b 'imp' (c 'imp' a)) . x = ('not' (b . x)) 'or' ((c 'imp' a) . x) by BVFUNC_1:def_8 .= ('not' (b . x)) 'or' (('not' (c . x)) 'or' (a . x)) by BVFUNC_1:def_8 .= TRUE by A2, BINARITH:11 ; hence (b 'imp' (c 'imp' a)) . x = TRUE ; ::_thesis: verum end; hence b 'imp' (c 'imp' a) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:24 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y & b = I_el Y holds c 'imp' a = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st c 'imp' (b 'imp' a) = I_el Y & b = I_el Y holds c 'imp' a = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( c 'imp' (b 'imp' a) = I_el Y & b = I_el Y implies c 'imp' a = I_el Y ) assume that A1: c 'imp' (b 'imp' a) = I_el Y and A2: b = I_el Y ; ::_thesis: c 'imp' a = I_el Y for x being Element of Y holds (c 'imp' a) . x = TRUE proof let x be Element of Y; ::_thesis: (c 'imp' a) . x = TRUE (c 'imp' (b 'imp' a)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (c . x)) 'or' ((b 'imp' a) . x) = TRUE by BVFUNC_1:def_8; then A3: ('not' (c . x)) 'or' (('not' (b . x)) 'or' (a . x)) = TRUE by BVFUNC_1:def_8; ('not' (c . x)) 'or' (FALSE 'or' (a . x)) = TRUE by A3, MARGREL1:11, A2, BVFUNC_1:def_11; then ('not' (c . x)) 'or' (a . x) = TRUE by BINARITH:3; hence (c 'imp' a) . x = TRUE by BVFUNC_1:def_8; ::_thesis: verum end; hence c 'imp' a = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem Th25: :: BVFUNC_5:25 for Y being non empty set for a being Function of Y,BOOLEAN st (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y holds a = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN st (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y holds a = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: ( (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y implies a = I_el Y ) assume (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y ; ::_thesis: a = I_el Y then (I_el Y) 'imp' a = I_el Y by Th2; hence a = I_el Y by Th2; ::_thesis: verum end; theorem :: BVFUNC_5:26 for Y being non empty set for b, c being Function of Y,BOOLEAN st b 'imp' (b 'imp' c) = I_el Y holds b 'imp' c = I_el Y proof let Y be non empty set ; ::_thesis: for b, c being Function of Y,BOOLEAN st b 'imp' (b 'imp' c) = I_el Y holds b 'imp' c = I_el Y let b, c be Function of Y,BOOLEAN; ::_thesis: ( b 'imp' (b 'imp' c) = I_el Y implies b 'imp' c = I_el Y ) assume A1: b 'imp' (b 'imp' c) = I_el Y ; ::_thesis: b 'imp' c = I_el Y for x being Element of Y holds (b 'imp' c) . x = TRUE proof let x be Element of Y; ::_thesis: (b 'imp' c) . x = TRUE A2: (b 'imp' c) . x = ('not' (b . x)) 'or' (c . x) by BVFUNC_1:def_8; (b 'imp' (b 'imp' c)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (b . x)) 'or' ((b 'imp' c) . x) = TRUE by BVFUNC_1:def_8; then ('not' (b . x)) 'or' (('not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def_8; then A3: (('not' (b . x)) 'or' ('not' (b . x))) 'or' (c . x) = TRUE by BINARITH:11; A4: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(b_._x)_=_TRUE_&_(b_'imp'_c)_._x_=_TRUE_)_or_(_c_._x_=_TRUE_&_(b_'imp'_c)_._x_=_TRUE_)_) percases ( 'not' (b . x) = TRUE or c . x = TRUE ) by A3, A4, BINARITH:3; case 'not' (b . x) = TRUE ; ::_thesis: (b 'imp' c) . x = TRUE hence (b 'imp' c) . x = TRUE by A2, BINARITH:10; ::_thesis: verum end; case c . x = TRUE ; ::_thesis: (b 'imp' c) . x = TRUE hence (b 'imp' c) . x = TRUE by A2, BINARITH:10; ::_thesis: verum end; end; end; hence (b 'imp' c) . x = TRUE ; ::_thesis: verum end; hence b 'imp' c = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:27 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y holds (a 'imp' b) 'imp' (a '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' (b 'imp' c) = I_el Y holds (a 'imp' b) 'imp' (a 'imp' c) = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' (b 'imp' c) = I_el Y implies (a 'imp' b) 'imp' (a 'imp' c) = I_el Y ) assume A1: a 'imp' (b 'imp' c) = I_el Y ; ::_thesis: (a 'imp' b) 'imp' (a 'imp' c) = I_el Y for x being Element of Y holds ((a 'imp' b) 'imp' (a 'imp' c)) . x = TRUE proof let x be Element of Y; ::_thesis: ((a 'imp' b) 'imp' (a 'imp' c)) . x = TRUE A2: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; (a 'imp' (b 'imp' c)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (a . x)) 'or' ((b 'imp' c) . x) = TRUE by BVFUNC_1:def_8; then A3: ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def_8; ((a 'imp' b) 'imp' (a 'imp' c)) . x = ('not' ((a 'imp' b) . x)) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (b . x))) 'or' ((a 'imp' c) . x) by BVFUNC_1:def_8 .= (('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' (('not' (a . x)) 'or' (c . x)) by BVFUNC_1:def_8 .= ((('not' (a . x)) 'or' (c . x)) 'or' (a . x)) '&' ((('not' (a . x)) 'or' (c . x)) 'or' ('not' (b . x))) by XBOOLEAN:9 .= TRUE '&' ((('not' (a . x)) 'or' (c . x)) 'or' (a . x)) by A3, BINARITH:11 .= ((c . x) 'or' ('not' (a . x))) 'or' (a . x) by MARGREL1:14 .= (c . x) 'or' TRUE by A2, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((a 'imp' b) 'imp' (a 'imp' c)) . x = TRUE ; ::_thesis: verum end; hence (a 'imp' b) 'imp' (a 'imp' c) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:28 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y holds a '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' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y holds a 'imp' c = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y implies a 'imp' c = I_el Y ) assume ( a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y ) ; ::_thesis: a 'imp' c = I_el Y then (I_el Y) 'imp' ((I_el Y) 'imp' (a 'imp' c)) = I_el Y by Th21; hence a 'imp' c = I_el Y by Th25; ::_thesis: verum end; theorem :: BVFUNC_5:29 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y & a = I_el Y holds 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 'imp' c) = I_el Y & a 'imp' b = I_el Y & a = I_el Y holds c = I_el Y let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' (b 'imp' c) = I_el Y & a 'imp' b = I_el Y & a = I_el Y implies c = I_el Y ) assume that A1: a 'imp' (b 'imp' c) = I_el Y and A2: a 'imp' b = I_el Y and A3: a = I_el Y ; ::_thesis: c = I_el Y for x being Element of Y holds c . x = TRUE proof let x be Element of Y; ::_thesis: c . x = TRUE (a 'imp' (b 'imp' c)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (a . x)) 'or' ((b 'imp' c) . x) = TRUE by BVFUNC_1:def_8; then A5: ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def_8; (a 'imp' b) . x = TRUE by A2, BVFUNC_1:def_11; then ('not' (a . x)) 'or' (b . x) = TRUE by BVFUNC_1:def_8; then FALSE 'or' (b . x) = TRUE by A3, BVFUNC_1:def_11, MARGREL1:11; then b . x = TRUE by BINARITH:3; then FALSE 'or' (('not' TRUE) 'or' (c . x)) = TRUE by A5, A3, BVFUNC_1:def_11, MARGREL1:11; then FALSE 'or' (FALSE 'or' (c . x)) = TRUE by MARGREL1:11; then FALSE 'or' (c . x) = TRUE by BINARITH:3; hence c . x = TRUE by BINARITH:3; ::_thesis: verum end; hence c = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:30 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a 'imp' (b 'imp' c) = I_el Y & a 'imp' (c 'imp' d) = I_el Y holds a 'imp' (b 'imp' 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 'imp' c) = I_el Y & a 'imp' (c 'imp' d) = I_el Y holds a 'imp' (b 'imp' d) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' (b 'imp' c) = I_el Y & a 'imp' (c 'imp' d) = I_el Y implies a 'imp' (b 'imp' d) = I_el Y ) assume that A1: a 'imp' (b 'imp' c) = I_el Y and A2: a 'imp' (c 'imp' d) = I_el Y ; ::_thesis: a 'imp' (b 'imp' d) = I_el Y for x being Element of Y holds (a 'imp' (b 'imp' d)) . x = TRUE proof let x be Element of Y; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE A3: (a 'imp' (b 'imp' d)) . x = ('not' (a . x)) 'or' ((b 'imp' d) . x) by BVFUNC_1:def_8 .= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (d . x)) by BVFUNC_1:def_8 ; (a 'imp' (c 'imp' d)) . x = TRUE by A2, BVFUNC_1:def_11; then ('not' (a . x)) 'or' ((c 'imp' d) . x) = TRUE by BVFUNC_1:def_8; then A4: ('not' (a . x)) 'or' (('not' (c . x)) 'or' (d . x)) = TRUE by BVFUNC_1:def_8; (a 'imp' (b 'imp' c)) . x = TRUE by A1, BVFUNC_1:def_11; then ('not' (a . x)) 'or' ((b 'imp' c) . x) = TRUE by BVFUNC_1:def_8; then A5: ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def_8; A6: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_'not'_(a_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_'not'_(a_._x)_=_TRUE_&_('not'_(c_._x))_'or'_(d_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_('not'_(b_._x))_'or'_(c_._x)_=_TRUE_&_'not'_(a_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_('not'_(b_._x))_'or'_(c_._x)_=_TRUE_&_('not'_(c_._x))_'or'_(d_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_) percases ( ( 'not' (a . x) = TRUE & 'not' (a . x) = TRUE ) or ( 'not' (a . x) = TRUE & ('not' (c . x)) 'or' (d . x) = TRUE ) or ( ('not' (b . x)) 'or' (c . x) = TRUE & 'not' (a . x) = TRUE ) or ( ('not' (b . x)) 'or' (c . x) = TRUE & ('not' (c . x)) 'or' (d . x) = TRUE ) ) by A5, A6, A4, BINARITH:3; case ( 'not' (a . x) = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE hence (a 'imp' (b 'imp' d)) . x = TRUE by A3, BINARITH:10; ::_thesis: verum end; case ( 'not' (a . x) = TRUE & ('not' (c . x)) 'or' (d . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE hence (a 'imp' (b 'imp' d)) . x = TRUE by A3, BINARITH:10; ::_thesis: verum end; case ( ('not' (b . x)) 'or' (c . x) = TRUE & 'not' (a . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE hence (a 'imp' (b 'imp' d)) . x = TRUE by A3, BINARITH:10; ::_thesis: verum end; caseA7: ( ('not' (b . x)) 'or' (c . x) = TRUE & ('not' (c . x)) 'or' (d . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE A8: ( 'not' (c . x) = TRUE or 'not' (c . x) = FALSE ) by XBOOLEAN:def_3; A9: ( 'not' (b . x) = TRUE or 'not' (b . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(b_._x)_=_TRUE_&_'not'_(c_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_'not'_(b_._x)_=_TRUE_&_d_._x_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_c_._x_=_TRUE_&_'not'_(c_._x)_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_or_(_c_._x_=_TRUE_&_d_._x_=_TRUE_&_(a_'imp'_(b_'imp'_d))_._x_=_TRUE_)_) percases ( ( 'not' (b . x) = TRUE & 'not' (c . x) = TRUE ) or ( 'not' (b . x) = TRUE & d . x = TRUE ) or ( c . x = TRUE & 'not' (c . x) = TRUE ) or ( c . x = TRUE & d . x = TRUE ) ) by A7, A9, A8, BINARITH:3; case ( 'not' (b . x) = TRUE & 'not' (c . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE then (a 'imp' (b 'imp' d)) . x = ('not' (a . x)) 'or' TRUE by A3, BINARITH:10 .= TRUE by BINARITH:10 ; hence (a 'imp' (b 'imp' d)) . x = TRUE ; ::_thesis: verum end; case ( 'not' (b . x) = TRUE & d . x = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE hence (a 'imp' (b 'imp' d)) . x = TRUE by A3, BINARITH:10; ::_thesis: verum end; case ( c . x = TRUE & 'not' (c . x) = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE hence (a 'imp' (b 'imp' d)) . x = TRUE by MARGREL1:11; ::_thesis: verum end; case ( c . x = TRUE & d . x = TRUE ) ; ::_thesis: (a 'imp' (b 'imp' d)) . x = TRUE then (a 'imp' (b 'imp' d)) . x = ('not' (a . x)) 'or' TRUE by A3, BINARITH:10 .= TRUE by BINARITH:10 ; hence (a 'imp' (b 'imp' d)) . x = TRUE ; ::_thesis: verum end; end; end; hence (a 'imp' (b 'imp' d)) . x = TRUE ; ::_thesis: verum end; end; end; hence (a 'imp' (b 'imp' d)) . x = TRUE ; ::_thesis: verum end; hence a 'imp' (b 'imp' d) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:31 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (('not' a) 'imp' ('not' b)) 'imp' (b 'imp' a) = 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' (b 'imp' a) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'imp' ('not' b)) 'imp' (b 'imp' a) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((('not' a) 'imp' ('not' b)) 'imp' (b 'imp' a)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; ((('not' a) 'imp' ('not' b)) 'imp' (b 'imp' a)) . x = ('not' ((('not' a) 'imp' ('not' b)) . x)) 'or' ((b 'imp' a) . x) by BVFUNC_1:def_8 .= ('not' (('not' (('not' a) . x)) 'or' (('not' b) . x))) 'or' ((b 'imp' a) . x) by BVFUNC_1:def_8 .= (('not' ('not' (('not' a) . x))) '&' ('not' (('not' b) . x))) 'or' (('not' (b . x)) 'or' (a . x)) by BVFUNC_1:def_8 .= ((('not' (b . x)) 'or' (a . x)) 'or' (('not' a) . x)) '&' ((('not' (b . x)) 'or' (a . x)) 'or' ('not' (('not' b) . x))) by XBOOLEAN:9 .= (('not' (b . x)) 'or' ((a . x) 'or' (('not' a) . x))) '&' ((('not' (b . x)) 'or' (a . x)) 'or' ('not' (('not' b) . x))) by BINARITH:11 .= (('not' (b . x)) 'or' TRUE) '&' ((('not' (b . x)) 'or' (a . x)) 'or' ('not' (('not' b) . x))) by A5, MARGREL1:def_19 .= TRUE '&' ((('not' (b . x)) 'or' (a . x)) 'or' ('not' (('not' b) . x))) by BINARITH:10 .= ((a . x) 'or' ('not' (b . x))) 'or' ('not' (('not' b) . x)) by MARGREL1:14 .= (a . x) 'or' (('not' (b . x)) 'or' ('not' (('not' b) . x))) by BINARITH:11 .= (a . x) 'or' TRUE by A6, MARGREL1:def_19 .= TRUE by BINARITH:10 ; hence ((('not' a) 'imp' ('not' b)) 'imp' (b 'imp' a)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:32 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('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) 'imp' (('not' b) 'imp' ('not' a)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) 'imp' (('not' b) 'imp' ('not' a)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' b) 'imp' (('not' b) 'imp' ('not' a))) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; ((a 'imp' b) 'imp' (('not' b) 'imp' ('not' a))) . x = ('not' ((a 'imp' b) . x)) 'or' ((('not' b) 'imp' ('not' a)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (b . x))) 'or' ((('not' b) 'imp' ('not' a)) . x) by BVFUNC_1:def_8 .= (('not' ('not' (a . x))) '&' ('not' (b . x))) 'or' (('not' (('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_19 .= ((b . x) 'or' ('not' (a . x))) 'or' ((a . x) '&' ('not' (b . x))) by MARGREL1:def_19 .= (((b . x) 'or' ('not' (a . x))) 'or' (a . x)) '&' (((b . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) by XBOOLEAN:9 .= ((b . x) 'or' TRUE) '&' (((b . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) by A5, BINARITH:11 .= TRUE '&' (((b . x) 'or' ('not' (a . x))) 'or' ('not' (b . x))) by BINARITH:10 .= (('not' (a . x)) 'or' (b . x)) 'or' ('not' (b . x)) by MARGREL1:14 .= ('not' (a . x)) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((a 'imp' b) 'imp' (('not' b) 'imp' ('not' a))) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:33 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (a 'imp' ('not' b)) 'imp' (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' ('not' b)) 'imp' (b 'imp' ('not' a)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' ('not' b)) 'imp' (b 'imp' ('not' a)) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' ('not' b)) 'imp' (b 'imp' ('not' a))) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; ((a 'imp' ('not' b)) 'imp' (b 'imp' ('not' a))) . x = ('not' ((a 'imp' ('not' b)) . x)) 'or' ((b 'imp' ('not' a)) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (('not' b) . x))) 'or' ((b 'imp' ('not' a)) . x) by BVFUNC_1:def_8 .= (('not' ('not' (a . x))) '&' ('not' (('not' b) . x))) 'or' (('not' (b . x)) 'or' (('not' a) . x)) by BVFUNC_1:def_8 .= ((a . x) '&' ('not' ('not' (b . x)))) 'or' (('not' (b . x)) 'or' (('not' a) . x)) by MARGREL1:def_19 .= (('not' (b . x)) 'or' ('not' (a . x))) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_19 .= ((('not' (b . x)) 'or' ('not' (a . x))) 'or' (a . x)) '&' ((('not' (b . x)) 'or' ('not' (a . x))) 'or' (b . x)) by XBOOLEAN:9 .= (('not' (b . x)) 'or' TRUE) '&' ((('not' (b . x)) 'or' ('not' (a . x))) 'or' (b . x)) by A5, BINARITH:11 .= TRUE '&' ((('not' (b . x)) 'or' ('not' (a . x))) 'or' (b . x)) by BINARITH:10 .= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (b . x) by MARGREL1:14 .= ('not' (a . x)) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((a 'imp' ('not' b)) 'imp' (b 'imp' ('not' a))) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:34 for Y being non empty set for a, b being Function of Y,BOOLEAN holds (('not' a) 'imp' b) 'imp' (('not' b) 'imp' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (('not' a) 'imp' b) 'imp' (('not' b) 'imp' a) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: (('not' a) 'imp' b) 'imp' (('not' b) 'imp' a) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((('not' a) 'imp' b) 'imp' (('not' b) 'imp' a)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; A6: now__::_thesis:_(_(_b_._x_=_TRUE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_or_(_b_._x_=_FALSE_&_('not'_(b_._x))_'or'_(b_._x)_=_TRUE_)_) percases ( b . x = TRUE or b . x = FALSE ) by XBOOLEAN:def_3; case b . x = TRUE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE hence ('not' (b . x)) 'or' (b . x) = TRUE by BINARITH:10; ::_thesis: verum end; case b . x = FALSE ; ::_thesis: ('not' (b . x)) 'or' (b . x) = TRUE then ('not' (b . x)) 'or' (b . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (b . x)) 'or' (b . x) = TRUE ; ::_thesis: verum end; end; end; ((('not' a) 'imp' b) 'imp' (('not' b) 'imp' a)) . x = ('not' ((('not' a) 'imp' b) . x)) 'or' ((('not' b) 'imp' a) . x) by BVFUNC_1:def_8 .= ('not' (('not' (('not' a) . x)) 'or' (b . x))) 'or' ((('not' b) 'imp' a) . x) by BVFUNC_1:def_8 .= (('not' ('not' (('not' a) . x))) '&' ('not' (b . x))) 'or' (('not' (('not' b) . x)) 'or' (a . x)) by BVFUNC_1:def_8 .= (('not' (a . x)) '&' ('not' (b . x))) 'or' (('not' (('not' b) . x)) 'or' (a . x)) by MARGREL1:def_19 .= ((b . x) 'or' (a . x)) 'or' (('not' (a . x)) '&' ('not' (b . x))) by MARGREL1:def_19 .= (((b . x) 'or' (a . x)) 'or' ('not' (a . x))) '&' (((b . x) 'or' (a . x)) 'or' ('not' (b . x))) by XBOOLEAN:9 .= ((b . x) 'or' TRUE) '&' (((b . x) 'or' (a . x)) 'or' ('not' (b . x))) by A5, BINARITH:11 .= TRUE '&' (((b . x) 'or' (a . x)) 'or' ('not' (b . x))) by BINARITH:10 .= ((a . x) 'or' (b . x)) 'or' ('not' (b . x)) by MARGREL1:14 .= (a . x) 'or' TRUE by A6, BINARITH:11 .= TRUE by BINARITH:10 ; hence ((('not' a) 'imp' b) 'imp' (('not' b) 'imp' a)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:35 for Y being non empty set for a being Function of Y,BOOLEAN holds (a 'imp' ('not' a)) 'imp' ('not' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds (a 'imp' ('not' a)) 'imp' ('not' a) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: (a 'imp' ('not' a)) 'imp' ('not' a) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: ((a 'imp' ('not' a)) 'imp' ('not' a)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; ((a 'imp' ('not' a)) 'imp' ('not' a)) . x = ('not' ((a 'imp' ('not' a)) . x)) 'or' (('not' a) . x) by BVFUNC_1:def_8 .= ('not' (('not' (a . x)) 'or' (('not' a) . x))) 'or' (('not' a) . x) by BVFUNC_1:def_8 .= ((a . x) '&' ('not' ('not' (a . x)))) 'or' (('not' a) . x) by MARGREL1:def_19 .= TRUE by A5, MARGREL1:def_19 ; hence ((a 'imp' ('not' a)) 'imp' ('not' a)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:36 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (a 'imp' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ('not' a) 'imp' (a 'imp' b) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ('not' a) 'imp' (a 'imp' b) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (('not' a) 'imp' (a 'imp' b)) . x = (I_el Y) . x A5: now__::_thesis:_(_(_a_._x_=_TRUE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_or_(_a_._x_=_FALSE_&_('not'_(a_._x))_'or'_(a_._x)_=_TRUE_)_) percases ( a . x = TRUE or a . x = FALSE ) by XBOOLEAN:def_3; case a . x = TRUE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE hence ('not' (a . x)) 'or' (a . x) = TRUE by BINARITH:10; ::_thesis: verum end; case a . x = FALSE ; ::_thesis: ('not' (a . x)) 'or' (a . x) = TRUE then ('not' (a . x)) 'or' (a . x) = TRUE 'or' FALSE by MARGREL1:11 .= TRUE by BINARITH:10 ; hence ('not' (a . x)) 'or' (a . x) = TRUE ; ::_thesis: verum end; end; end; (('not' a) 'imp' (a 'imp' b)) . x = ('not' (('not' a) . x)) 'or' ((a 'imp' b) . x) by BVFUNC_1:def_8 .= ('not' (('not' a) . x)) 'or' (('not' (a . x)) 'or' (b . x)) by BVFUNC_1:def_8 .= (a . x) 'or' (('not' (a . x)) 'or' (b . x)) by MARGREL1:def_19 .= TRUE 'or' (b . x) by A5, BINARITH:11 .= TRUE by BINARITH:10 ; hence (('not' a) 'imp' (a 'imp' b)) . x = (I_el Y) . x by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_5:37 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds 'not' ((a '&' b) '&' c) = (('not' a) 'or' ('not' b)) 'or' ('not' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds 'not' ((a '&' b) '&' c) = (('not' a) 'or' ('not' b)) 'or' ('not' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: 'not' ((a '&' b) '&' c) = (('not' a) 'or' ('not' b)) 'or' ('not' c) 'not' ((a '&' b) '&' c) = ('not' (a '&' b)) 'or' ('not' c) by BVFUNC_1:14 .= (('not' a) 'or' ('not' b)) 'or' ('not' c) by BVFUNC_1:14 ; hence 'not' ((a '&' b) '&' c) = (('not' a) 'or' ('not' b)) 'or' ('not' c) ; ::_thesis: verum end; theorem :: BVFUNC_5:38 for Y being non empty set for a, b, c being Function of Y,BOOLEAN holds 'not' ((a 'or' b) 'or' c) = (('not' a) '&' ('not' b)) '&' ('not' c) proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds 'not' ((a 'or' b) 'or' c) = (('not' a) '&' ('not' b)) '&' ('not' c) let a, b, c be Function of Y,BOOLEAN; ::_thesis: 'not' ((a 'or' b) 'or' c) = (('not' a) '&' ('not' b)) '&' ('not' c) 'not' ((a 'or' b) 'or' c) = ('not' (a 'or' b)) '&' ('not' c) by BVFUNC_1:13 .= (('not' a) '&' ('not' b)) '&' ('not' c) by BVFUNC_1:13 ; hence 'not' ((a 'or' b) 'or' c) = (('not' a) '&' ('not' b)) '&' ('not' c) ; ::_thesis: verum end; theorem :: BVFUNC_5:39 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) a 'or' ((b '&' c) '&' d) = (a 'or' (b '&' c)) '&' (a 'or' d) by BVFUNC_1:11 .= ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) by BVFUNC_1:11 ; hence a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) ; ::_thesis: verum end; theorem :: BVFUNC_5:40 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN holds a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) a '&' ((b 'or' c) 'or' d) = (a '&' (b 'or' c)) 'or' (a '&' d) by BVFUNC_1:12 .= ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) by BVFUNC_1:12 ; hence a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) ; ::_thesis: verum end;