A1: 'not' . 1 = 1 ;
'&' . 1 = 2 ;
hence ( 'not' <> '&' & 'not' <> '=' & '&' <> '=' ) by A1, FINSEQ_1:def 8; :: thesis: verum