let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds
q in TAUT Al
let p, q be Element of CQC-WFF Al; :: thesis: ( p in TAUT Al & p => q in TAUT Al implies q in TAUT Al )
TAUT Al is being_a_theory by Th11;
hence ( p in TAUT Al & p => q in TAUT Al implies q in TAUT Al ) ; :: thesis: verum