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