let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y
let a, b, c be Function of Y,BOOLEAN; :: thesis: ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y
b 'imp' (a 'imp' b) = I_el Y by Th15;
hence ((a 'imp' b) 'imp' c) 'imp' (b 'imp' c) = I_el Y by Th14; :: thesis: verum