let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF holds ('not' p) . x = 'not' (p . x)
let p be Element of QC-WFF ; :: thesis: ('not' p) . x = 'not' (p . x)
set 'p = 'not' p;
A1: 'not' p is negative by QC_LANG1:def 18;
then the_argument_of ('not' p) = p by QC_LANG1:def 23;
hence ('not' p) . x = 'not' (p . x) by A1, Th31; :: thesis: verum