let Y be non empty set ; :: thesis: for a being Element of Funcs (Y,BOOLEAN) st (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y holds
a = I_el Y
let a be Element of Funcs (Y,BOOLEAN); :: thesis: ( (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y implies a = I_el Y )
assume (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y ; :: thesis: a = I_el Y
then (I_el Y) 'imp' a = I_el Y by Th2;
hence a = I_el Y by Th2; :: thesis: verum