let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds ('not' (All x,p)) <=> (Ex x,('not' p)) is valid
let x be bound_QC-variable; :: thesis: ('not' (All x,p)) <=> (Ex x,('not' p)) is valid
( ('not' (All x,p)) => (Ex x,('not' p)) is valid & (Ex x,('not' p)) => ('not' (All x,p)) is valid ) by Th55;
hence ('not' (All x,p)) <=> (Ex x,('not' p)) is valid by Lm14; :: thesis: verum