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