let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds
( (Ex x,('not' ('not' p))) => (Ex x,p) is valid & (Ex x,p) => (Ex x,('not' ('not' p))) is valid )
let x be bound_QC-variable; :: thesis: ( (Ex x,('not' ('not' p))) => (Ex x,p) is valid & (Ex x,p) => (Ex x,('not' ('not' p))) is valid )
( ('not' ('not' p)) => p is valid & p => ('not' ('not' p)) is valid ) by LUKASI_1:64, LUKASI_1:65;
then ( All x,(('not' ('not' p)) => p) is valid & All x,(p => ('not' ('not' p))) is valid ) by Th26;
hence ( (Ex x,('not' ('not' p))) => (Ex x,p) is valid & (Ex x,p) => (Ex x,('not' ('not' p))) is valid ) by Th39; :: thesis: verum