let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds a = (a 'imp' b) 'imp' a
let a, b be Function of Y,BOOLEAN; :: thesis: a = (a 'imp' b) 'imp' a
((a 'imp' b) 'imp' a) 'imp' a = I_el Y by BVFUNC_6:100;
then A1: (a 'imp' b) 'imp' a '<' a by BVFUNC_1:16;
a 'imp' ((a 'imp' b) 'imp' a) = I_el Y by Th32;
then a '<' (a 'imp' b) 'imp' a by BVFUNC_1:16;
hence a = (a 'imp' b) 'imp' a by A1, BVFUNC_1:15; :: thesis: verum