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
p '&' q = <*2*> ^ (p ^ q) by FINSEQ_1:45;
then A1: ( (p '&' q) . 1 = 2 & (prop n) . 1 = 3 + n ) by FINSEQ_1:57, FINSEQ_1:58;

now

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

end;

hence p '&' q <> prop n by A1; :: thesis: verum