let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x)
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x)
let p be Element of QC-WFF A; :: thesis: ('not' p) . x = 'not' (p . x)
set 9p = 'not' p;
A1: 'not' p is negative by QC_LANG1:def 19;
then the_argument_of ('not' p) = p by QC_LANG1:def 24;
hence ('not' p) . x = 'not' (p . x) by A1, Th18; :: thesis: verum