let T, S be Subset of CQC-WFF ; ( 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
; T /\ S is being_a_theory
A3:
( VERUM in T & VERUM in S )
by A1, A2, Def1;
thus
VERUM in T /\ S
by A3, XBOOLE_0:def 4; CQC_THE1:def 1 for p, q, r being Element of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & 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 ; for s being QC-formula
for x, y being bound_QC-variable 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
let s be QC-formula; for x, y being bound_QC-variable 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 & s . y in CQC-WFF & 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; ( (('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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A4:
( (('not' p) => p) => p in T & (('not' p) => p) => p in S )
by A1, A2, Def1;
thus
(('not' p) => p) => p in T /\ S
by A4, XBOOLE_0:def 4; ( 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A5:
( p => (('not' p) => q) in T & p => (('not' p) => q) in S )
by A1, A2, Def1;
thus
p => (('not' p) => q) in T /\ S
by A5, XBOOLE_0:def 4; ( (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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A6:
( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in S )
by A1, A2, Def1;
thus
(p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S
by A6, XBOOLE_0:def 4; ( (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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A7:
( (p '&' q) => (q '&' p) in T & (p '&' q) => (q '&' p) in S )
by A1, A2, Def1;
thus
(p '&' q) => (q '&' p) in T /\ S
by A7, XBOOLE_0:def 4; ( ( 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A8:
( p in T & p => q in T implies q in T )
by A1, Def1;
A9:
( p in S & p => q in S implies q in S )
by A2, Def1;
thus
( p in T /\ S & p => q in T /\ S implies q in T /\ S )
by A8, A9, XBOOLE_0:def 4; ( (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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A10:
( (All x,p) => p in T & (All x,p) => p in S )
by A1, A2, Def1;
thus
(All x,p) => p in T /\ S
by A10, XBOOLE_0:def 4; ( ( 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 & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) )
A11:
( p => q in T & not x in still_not-bound_in p implies p => (All x,q) in T )
by A1, Def1;
A12:
( p => q in S & not x in still_not-bound_in p implies p => (All x,q) in S )
by A2, Def1;
thus
( p => q in T /\ S & not x in still_not-bound_in p implies p => (All x,q) in T /\ S )
by A11, A12, XBOOLE_0:def 4; ( 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 )
A13:
( 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 )
by A1, Def1;
A14:
( 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 A2, Def1;
thus
( 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 A13, A14, XBOOLE_0:def 4; verum