let p, q be Element of HP-WFF ; :: thesis: p => q <> VERUM
p => q = <*1*> ^ (p ^ q) by FINSEQ_1:45;
then (p => q) . 1 = 1 by FINSEQ_1:58;
hence p => q <> VERUM by FINSEQ_1:57; :: thesis: verum