let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
let x be bound_QC-variable of Al; :: thesis: ( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
thus ( X |- 'not' (Ex (x,('not' p))) implies X |- All (x,p) ) :: thesis: ( X |- All (x,p) implies X |- 'not' (Ex (x,('not' p))) )

proof

assume X |- 'not' (Ex (x,('not' p))) ; :: thesis: X |- All (x,p)
then consider f1 being FinSequence of CQC-WFF Al such that
A1: rng f1 c= X and
A2: |- f1 ^ <*('not' (Ex (x,('not' p))))*> by HENMODEL:def 1;
|- f1 ^ <*(All (x,p))*> by A2, CALCUL_1:68;
hence X |- All (x,p) by A1, HENMODEL:def 1; :: thesis: verum

end;

thus ( X |- All (x,p) implies X |- 'not' (Ex (x,('not' p))) ) :: thesis: verum

proof

assume X |- All (x,p) ; :: thesis: X |- 'not' (Ex (x,('not' p)))
then consider f1 being FinSequence of CQC-WFF Al such that
A3: rng f1 c= X and
A4: |- f1 ^ <*(All (x,p))*> by HENMODEL:def 1;
|- f1 ^ <*('not' (Ex (x,('not' p))))*> by A4, CALCUL_1:68;
hence X |- 'not' (Ex (x,('not' p))) by A3, HENMODEL:def 1; :: thesis: verum

end;