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

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