let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) )
thus ( a 'eqv' b = I_el Y implies ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) :: thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y implies a 'eqv' b = I_el Y )

proof

assume a 'eqv' b = I_el Y ; :: thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y )
then a = b by BVFUNC_1:17;
hence ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) by BVFUNC_1:16; :: thesis: verum

end;

assume ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ; :: thesis: a 'eqv' b = I_el Y
then a 'eqv' b = (I_el Y) '&' (I_el Y) by Th7;
hence a 'eqv' b = I_el Y ; :: thesis: verum