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

proof

let t be Element of CQC-WFF A; :: thesis: ( t in Cn ({p} \/ {q}) iff for T being Subset of (CQC-WFF A) 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 A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) :: thesis: ( ( for T being Subset of (CQC-WFF A) 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 A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T
let T be Subset of (CQC-WFF A); :: 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 & TAUT A c= T ) by A2, A3, CQC_THE1:38, ZFMISC_1:31;
(p '&' q) => q in TAUT A by PROCAL_1:21;
then q in T by A2, A4, CQC_THE1:def 1;
then A5: {q} c= T by ZFMISC_1:31;
(p '&' q) => p in TAUT A by PROCAL_1:19;
then p in T by A2, A4, CQC_THE1:def 1;
then {p} c= T by ZFMISC_1:31;
then {p} \/ {q} c= T by A5, 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 A) st T is being_a_theory & {(p '&' q)} c= T holds
t in T ) implies t in Cn ({p} \/ {q}) ) :: thesis: verum

proof

assume A6: for T being Subset of (CQC-WFF A) 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 A) st T is being_a_theory & {p} \/ {q} c= T holds
t in T

proof

let T be Subset of (CQC-WFF A); :: thesis: ( T is being_a_theory & {p} \/ {q} c= T implies t in T )
assume that
A7: T is being_a_theory and
A8: {p} \/ {q} c= T ; :: thesis: t in T
{p} c= {p} \/ {q} by XBOOLE_1:7;
then {p} c= T by A8, XBOOLE_1:1;
then A9: p in T by ZFMISC_1:31;
{q} c= {p} \/ {q} by XBOOLE_1:7;
then {q} c= T by A8, XBOOLE_1:1;
then A10: q in T by ZFMISC_1:31;
( p => (q => (p '&' q)) in TAUT A & TAUT A c= T ) by A7, CQC_THE1:38, PROCAL_1:28;
then q => (p '&' q) in T by A7, A9, CQC_THE1:def 1;
then p '&' q in T by A7, A10, CQC_THE1:def 1;
then {(p '&' q)} c= T by ZFMISC_1:31;
hence t in T by A6, A7; :: 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