defpred S1[ set , set ] means for p being Element of CQC-WFF A st p = f . $1 holds
$2 = 'not' p;
A1: for e being Element of D ex u being Element of CQC-WFF A st S1[e,u]
proof
let e be Element of D; :: thesis: ex u being Element of CQC-WFF A st S1[e,u]
reconsider p = f . e as Element of CQC-WFF A ;
take 'not' p ; :: thesis: S1[e, 'not' p]
thus S1[e, 'not' p] ; :: thesis: verum
end;
consider F being Function of D,(CQC-WFF A) such that
A2: for e being Element of D holds S1[e,F . e] from FUNCT_2:sch 3(A1);
 F is Element of Funcs (D,(CQC-WFF A)) by FUNCT_2:8;
hence ex b1 being Element of Funcs (D,(CQC-WFF A)) st
for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
b1 . a = 'not' p by A2; :: thesis: verum