let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF holds Free (Ex x,p) = Free p
let p be Element of QC-WFF ; :: 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 Th50
.= Free ('not' p) by Th55
.= Free p by Th50 ;
:: thesis: verum