let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st p <==> q holds
Ex x,p <==> Ex x,q
let x be bound_QC-variable; :: thesis: ( p <==> q implies Ex x,p <==> Ex x,q )
assume p <==> q ; :: thesis: Ex x,p <==> Ex x,q
then 'not' p <==> 'not' q by Lm5;
then All x,('not' p) <==> All x,('not' q) by Th58;
then A1: 'not' (All x,('not' p)) <==> 'not' (All x,('not' q)) by Lm5;
Ex x,p = 'not' (All x,('not' p)) by QC_LANG2:def 5;
hence Ex x,p <==> Ex x,q by A1, QC_LANG2:def 5; :: thesis: verum