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