environ
vocabularies HIDDEN, SUBSET_1, CQC_LANG, QC_LANG1, FINSEQ_1, ZFMISC_1, CQC_THE1, NUMBERS, XBOOLEAN, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, RCOMP_1, MCART_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, FINSEQ_1, FUNCT_1, XTUPLE_0, MCART_1, DOMAIN_1, QC_LANG1, QC_LANG2, CQC_LANG, CQC_THE1, XXREAL_0;
definitions CQC_THE1;
theorems TARSKI, ZFMISC_1, LUKASI_1, CQC_LANG, CQC_THE1, ENUMSET1, QC_LANG1, QC_LANG2, QC_LANG3, PROCAL_1, XBOOLE_0, XBOOLE_1, XXREAL_0;
schemes NAT_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, CQC_LANG, ORDINAL1, LUKASI_1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, XREAL_0, CQC_THE1, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL;
equalities ;
expansions CQC_THE1;
Lm1:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
by PROCAL_1:19, PROCAL_1:21;
Lm2:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
Lm3:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds
p => (q '&' r) is valid
by PROCAL_1:52;
Lm4:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid
by PROCAL_1:57;
Lm5:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid
by PROCAL_1:56;
Lm6:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
by PROCAL_1:3, PROCAL_1:4;
Lm7:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid
by PROCAL_1:53;
Lm8:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
by PROCAL_1:47;
Lm9:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r '&' p) => (r '&' q) is valid
by PROCAL_1:50;
Lm10:
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid
by PROCAL_1:48;
Lm11:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
by PROCAL_1:5;
Lm12:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
Lm13:
for A being QC-alphabet
for p being Element of CQC-WFF A holds p <=> p is valid
Lm14:
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )
Lm15:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
Lm16:
for A being QC-alphabet
for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid
Lm17:
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(All (x,(p => q))) => (p => (All (x,q))) is valid