let A be QC-alphabet ; for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let p, q be Element of CQC-WFF A; for x being bound_QC-variable of A st p <==> q holds
Ex (x,p) <==> Ex (x,q)
let x be bound_QC-variable of A; ( p <==> q implies Ex (x,p) <==> Ex (x,q) )
assume
p <==> q
; 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; verum