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