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 9p = 'not' p;
A1: 'not' p is negative by QC_LANG1:def 17;
then the_argument_of ('not' p) = p by QC_LANG1:def 22;
hence ('not' p) . x = 'not' (p . x) by A1, Th31; :: thesis: verum