let Al be QC-alphabet ; :: thesis: for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds
T /\ S is being_a_theory

let T, S be Subset of (CQC-WFF Al); :: thesis: ( T is being_a_theory & S is being_a_theory implies T /\ S is being_a_theory )
assume that
A1: T is being_a_theory and
A2: S is being_a_theory ; :: thesis: T /\ S is being_a_theory
( VERUM Al in T & VERUM Al in S ) by A1, A2;
hence VERUM Al in T /\ S by XBOOLE_0:def 4; :: according to CQC_THE1:def 1 :: thesis: for p, q, r being Element of CQC-WFF Al
for s being QC-formula of Al
for x, y being bound_QC-variable of Al holds
( (() => p) => p in T /\ S & p => (() => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )

let p, q, r be Element of CQC-WFF Al; :: thesis: for s being QC-formula of Al
for x, y being bound_QC-variable of Al holds
( (() => p) => p in T /\ S & p => (() => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )

let s be QC-formula of Al; :: thesis: for x, y being bound_QC-variable of Al holds
( (() => p) => p in T /\ S & p => (() => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )

let x, y be bound_QC-variable of Al; :: thesis: ( (() => p) => p in T /\ S & p => (() => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
( (('not' p) => p) => p in T & (() => p) => p in S ) by A1, A2;
hence (('not' p) => p) => p in T /\ S by XBOOLE_0:def 4; :: thesis: ( p => (() => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
( p => (() => q) in T & p => (() => q) in S ) by A1, A2;
hence p => (() => q) in T /\ S by XBOOLE_0:def 4; :: thesis: ( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in S ) by A1, A2;
hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S by XBOOLE_0:def 4; :: thesis: ( (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
( (p '&' q) => (q '&' p) in T & (p '&' q) => (q '&' p) in S ) by A1, A2;
hence (p '&' q) => (q '&' p) in T /\ S by XBOOLE_0:def 4; :: thesis: ( ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A3: ( p in T & p => q in T implies q in T ) by A1;
( p in S & p => q in S implies q in S ) by A2;
hence ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) by ; :: thesis: ( (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
( (All (x,p)) => p in T & (All (x,p)) => p in S ) by A1, A2;
hence (All (x,p)) => p in T /\ S by XBOOLE_0:def 4; :: thesis: ( ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A4: ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) by A1;
( p => q in S & not x in still_not-bound_in p implies p => (All (x,q)) in S ) by A2;
hence ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) by ; :: thesis: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S )
A5: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) by A1;
( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in S implies s . y in S ) by A2;
hence ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) by ; :: thesis: verum