let p, q be Element of HP-WFF ; :: thesis: p => (q => p) is pseudo-canonical
reconsider s = p => (q => p) as canonical Element of HP-WFF by Th41;
s is pseudo-canonical ;
hence p => (q => p) is pseudo-canonical ; :: thesis: verum