let p, q be Element of CQC-WFF ; :: 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) \/ {p} |- q by A2, Def1;
then {} CQC-WFF |- p => q by A1, CQC_THE2:92;
hence p => q is valid by CQC_THE1:def 9; :: thesis: verum