let n be Element of NAT ; :: thesis: for p, q being Element of HP-WFF holds p => q <> prop n
let p, q be Element of HP-WFF ; :: thesis: p => q <> prop n

A1: now

assume 1 = (1 + 2) + n ; :: thesis: contradiction
then 1 + 0 = 1 + (2 + n) ;
hence contradiction ; :: thesis: verum

end;

p => q = <*1*> ^ (p ^ q) by FINSEQ_1:45;
then (p => q) . 1 = 1 by FINSEQ_1:58;
hence p => q <> prop n by A1, FINSEQ_1:57; :: thesis: verum