let p, q be Element of CQC-WFF ; :: thesis: Cn ({p} \/ {q}) = Cn {(p '&' q)}
for t being Element of CQC-WFF holds
( t in Cn ({p} \/ {q}) iff for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T )

proof

let t be Element of CQC-WFF ; :: thesis: ( t in Cn ({p} \/ {q}) iff for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T )
thus ( t in Cn ({p} \/ {q}) implies for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) :: thesis: ( ( for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) implies t in Cn ({p} \/ {q}) )

proof

assume A1: t in Cn ({p} \/ {q}) ; :: thesis: for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T
let T be Subset of CQC-WFF ; :: thesis: ( T is being_a_theory & {(p '&' q)} c= T implies t in T )
assume that
A2: T is being_a_theory and
A3: {(p '&' q)} c= T ; :: thesis: t in T
A4: p '&' q in T by A3, ZFMISC_1:37;
( (p '&' q) => p in TAUT & (p '&' q) => q in TAUT & TAUT c= T ) by A2, CQC_THE1:74, PROCAL_1:19, PROCAL_1:21;
then ( p in T & q in T ) by A2, A4, CQC_THE1:def 1;
then ( {p} c= T & {q} c= T ) by ZFMISC_1:37;
then {p} \/ {q} c= T by XBOOLE_1:8;
hence t in T by A1, A2, CQC_THE1:def 2; :: thesis: verum

end;

thus ( ( for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) implies t in Cn ({p} \/ {q}) ) :: thesis: verum

proof

assume A5: for T being Subset of CQC-WFF st T is being_a_theory & {(p '&' q)} c= T holds
t in T ; :: thesis: t in Cn ({p} \/ {q})
for T being Subset of CQC-WFF st T is being_a_theory & {p} \/ {q} c= T holds
t in T

proof

let T be Subset of CQC-WFF ; :: thesis: ( T is being_a_theory & {p} \/ {q} c= T implies t in T )
assume that
A6: T is being_a_theory and
A7: {p} \/ {q} c= T ; :: thesis: t in T
( {p} c= {p} \/ {q} & {q} c= {p} \/ {q} ) by XBOOLE_1:7;
then ( {p} c= T & {q} c= T ) by A7, XBOOLE_1:1;
then A8: ( p in T & q in T ) by ZFMISC_1:37;
( p => (q => (p '&' q)) in TAUT & TAUT c= T ) by A6, CQC_THE1:74, PROCAL_1:28;
then q => (p '&' q) in T by A6, A8, CQC_THE1:def 1;
then p '&' q in T by A6, A8, CQC_THE1:def 1;
then {(p '&' q)} c= T by ZFMISC_1:37;
hence t in T by A5, A6; :: thesis: verum

end;

hence t in Cn ({p} \/ {q}) by CQC_THE1:def 2; :: thesis: verum

end;

end;

hence Cn ({p} \/ {q}) = Cn {(p '&' q)} by CQC_THE1:def 2; :: thesis: verum