let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: a = (a 'imp' b) 'imp' a
a 'imp' ((a 'imp' b) 'imp' a) = I_el Y by Th33;
then A1: a '<' (a 'imp' b) 'imp' a by BVFUNC_1:19;
((a 'imp' b) 'imp' a) 'imp' a = I_el Y by BVFUNC_8:27;
then (a 'imp' b) 'imp' a '<' a by BVFUNC_1:19;
hence a = (a 'imp' b) 'imp' a by A1, BVFUNC_1:18; :: thesis: verum