let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
('not' a) 'eqv' ('not' b) = I_el Y
let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y implies ('not' a) 'eqv' ('not' b) = I_el Y )
assume a 'eqv' b = I_el Y ; :: thesis: ('not' a) 'eqv' ('not' b) = I_el Y
then a = b by BVFUNC_1:17;
hence ('not' a) 'eqv' ('not' b) = I_el Y by BVFUNC_1:17; :: thesis: verum