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 :: thesis: not 2 = (2 + 1) + n

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

end;

p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:32;
then (p '&' q) . 1 = 2 by FINSEQ_1:41;
hence p '&' q <> prop n by A1; :: thesis: verum