let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p
let p be Element of QC-WFF A; :: thesis: Free (Ex (x,p)) = Free p
Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def 5;
hence Free (Ex (x,p)) = Free (All (x,('not' p))) by Th39
.= Free ('not' p) by Th44
.= Free p by Th39 ;
:: thesis: verum