let X be Subset of CQC-WFF; :: thesis: for p, q being Element of CQC-WFF st p in Cn X & p => q in Cn X holds
q in Cn X
let p, q be Element of CQC-WFF ; :: 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 st T is being_a_theory & X c= T holds
q in T

proof

let T be Subset of CQC-WFF; :: 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, Def1; :: thesis: verum

end;

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