let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable holds ('not' p) . x,y = 'not' (p . x,y)
let x, y be bound_QC-variable; :: thesis: ('not' p) . x,y = 'not' (p . x,y)
set S = [p,(Sbst x,y)];
( [p,(Sbst x,y)] `1 = p & [p,(Sbst x,y)] `2 = Sbst x,y ) by MCART_1:7;
then ( ('not' p) . x,y = CQC_Sub [('not' p),(Sbst x,y)] & Sub_not [p,(Sbst x,y)] = [('not' p),(Sbst x,y)] ) by SUBSTUT1:def 20, SUBSTUT2:def 2;
then ('not' p) . x,y = 'not' (CQC_Sub [p,(Sbst x,y)]) by SUBSTUT1:29;
hence ('not' p) . x,y = 'not' (p . x,y) by SUBSTUT2:def 2; :: thesis: verum