let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st p => q is valid & not x in still_not-bound_in q holds
(Ex x,p) => q is valid
let x be bound_QC-variable; :: thesis: ( p => q is valid & not x in still_not-bound_in q implies (Ex x,p) => q is valid )
assume that
A1: p => q is valid and
A2: not x in still_not-bound_in q ; :: thesis: (Ex x,p) => q is valid
( ('not' q) => ('not' p) is valid & not x in still_not-bound_in ('not' q) ) by A1, A2, LUKASI_1:63, QC_LANG3:11;
then ('not' q) => (All x,('not' p)) is valid by CQC_THE1:106;
then ('not' (All x,('not' p))) => ('not' ('not' q)) is valid by LUKASI_1:63;
then (Ex x,p) => ('not' ('not' q)) is valid by QC_LANG2:def 5;
hence (Ex x,p) => q is valid by LUKASI_1:70; :: thesis: verum