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