let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF
for x being bound_QC-variable holds
( X |- 'not' (Ex x,('not' p)) iff X |- All x,p )
let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds
( X |- 'not' (Ex x,('not' p)) iff X |- All x,p )
let x be bound_QC-variable; :: 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 such that
A1: ( rng f1 c= X & |- f1 ^ <*('not' (Ex x,('not' p)))*> ) by HENMODEL:def 2;
|- f1 ^ <*(All x,p)*> by A1, CALCUL_1:68;
hence X |- All x,p by A1, HENMODEL:def 2; :: 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 such that
A2: ( rng f1 c= X & |- f1 ^ <*(All x,p)*> ) by HENMODEL:def 2;
|- f1 ^ <*('not' (Ex x,('not' p)))*> by A2, CALCUL_1:68;
hence X |- 'not' (Ex x,('not' p)) by A2, HENMODEL:def 2; :: thesis: verum

end;