let Y be non empty set ; :: thesis: (I_el Y) 'eqv' (I_el Y) = I_el Y
thus (I_el Y) 'eqv' (I_el Y) = 'not' ((I_el Y) 'xor' (I_el Y)) by Th12
.= 'not' ('not' (I_el Y)) by BVFUNC_6:87
.= I_el Y ; :: thesis: verum