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