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

( (('not' p) => p) => p in T /\ S & p => (('not' 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

( (('not' p) => p) => p in T /\ S & p => (('not' 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

( (('not' p) => p) => p in T /\ S & p => (('not' 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: ( (('not' p) => p) => p in T /\ S & p => (('not' 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 & (('not' p) => p) => p in S ) by A1, A2;

hence (('not' p) => p) => p in T /\ S by XBOOLE_0:def 4; :: thesis: ( p => (('not' 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 => (('not' p) => q) in T & p => (('not' p) => q) in S ) by A1, A2;

hence p => (('not' 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 A3, XBOOLE_0:def 4; :: 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 A4, XBOOLE_0:def 4; :: 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 A5, XBOOLE_0:def 4; :: thesis: verum

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

( (('not' p) => p) => p in T /\ S & p => (('not' 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

( (('not' p) => p) => p in T /\ S & p => (('not' 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

( (('not' p) => p) => p in T /\ S & p => (('not' 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: ( (('not' p) => p) => p in T /\ S & p => (('not' 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 & (('not' p) => p) => p in S ) by A1, A2;

hence (('not' p) => p) => p in T /\ S by XBOOLE_0:def 4; :: thesis: ( p => (('not' 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 => (('not' p) => q) in T & p => (('not' p) => q) in S ) by A1, A2;

hence p => (('not' 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 A3, XBOOLE_0:def 4; :: 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 A4, XBOOLE_0:def 4; :: 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 A5, XBOOLE_0:def 4; :: thesis: verum