let Al be QC-alphabet ; :: thesis:
let T, S be Subset of (CQC-WFF Al); :: thesis:
assume that
A1: T is being_a_theory and
A2: S is being_a_theory ; :: thesis:
( 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:
let p, q, r be Element of CQC-WFF Al; :: thesis:
let s be QC-formula of Al; :: thesis:
let x, y be bound_QC-variable of Al; :: thesis:
( (('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 & 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 & (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 & (p '&' q) => (q '&' p) in S ) by A1, A2;
hence (p '&' q) => (q '&' p) in T /\ S by XBOOLE_0:def 4; :: thesis:
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 & (All (x,p)) => p in S ) by A1, A2;
hence (All (x,p)) => p in T /\ S by XBOOLE_0:def 4; :: thesis:
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:
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: