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