let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds
p => q is valid
let p, q be Element of CQC-WFF A; :: thesis: ( p is closed & p |- q implies p => q is valid )
assume that
A1: p is closed and
A2: p |- q ; :: thesis: p => q is valid
({} (CQC-WFF A)) \/ {p} |- q by A2;
then {} (CQC-WFF A) |- p => q by A1, CQC_THE2:92;
hence p => q is valid by CQC_THE1:def 9; :: thesis: verum