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:96;
hence p => q is valid by CQC_THE1:def 10; :: thesis: verum