let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds (All x,('not' p)) <=> ('not' (Ex x,p)) is valid
let x be bound_QC-variable; :: thesis: (All x,('not' p)) <=> ('not' (Ex x,p)) is valid
('not' ('not' (All x,('not' p)))) => (All x,('not' p)) is valid by LUKASI_1:65;
then A1: ('not' (Ex x,p)) => (All x,('not' p)) is valid by QC_LANG2:def 5;
(All x,('not' p)) => ('not' ('not' (All x,('not' p)))) is valid by LUKASI_1:64;
then (All x,('not' p)) => ('not' (Ex x,p)) is valid by QC_LANG2:def 5;
hence (All x,('not' p)) <=> ('not' (Ex x,p)) is valid by A1, Lm14; :: thesis: verum