let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN st (I_el Y) 'imp' ((I_el Y) 'imp' a) = I_el Y holds
a = I_el Y
let a be Function of 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