let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds
q in Cn X
let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds
q in Cn X
let p, q be Element of CQC-WFF Al; :: thesis: ( p in Cn X & p => q in Cn X implies q in Cn X )
assume A1: ( p in Cn X & p => q in Cn X ) ; :: thesis: q in Cn X
for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
q in T

proof

let T be Subset of (CQC-WFF Al); :: thesis: ( T is being_a_theory & X c= T implies q in T )
assume that
A2: T is being_a_theory and
A3: X c= T ; :: thesis: q in T
( p in T & p => q in T ) by A1, A2, A3, Def2;
hence q in T by A2; :: thesis: verum

end;

hence q in Cn X by Def2; :: thesis: verum