environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, CQC_THE1, TARSKI, XBOOLE_0, XBOOLEAN, BVFUNC_2, RCOMP_1, XXREAL_0, FINSEQ_1, FUNCT_1, ARYTM_3, CARD_1, ZFREFLE1, FUNCOP_1, REALSET1, QC_LANG3, CQC_THE3, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, QC_LANG3, CQC_LANG, CQC_THE1, XXREAL_0;
definitions TARSKI;
theorems TARSKI, ZFMISC_1, CQC_THE1, CQC_THE2, LUKASI_1, NAT_1, QC_LANG1, QC_LANG2, QC_LANG3, PROCAL_1, CQC_LANG, XBOOLE_0, XBOOLE_1;
schemes NAT_1, QC_LANG1;
registrations SUBSET_1, RELSET_1, MEMBERED, CQC_LANG, LUKASI_1, XXREAL_0, NAT_1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, NAT_1, MEMBERED, QC_LANG3, CQC_THE1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;
Lm1:
for A being QC-alphabet
for X, Y being Subset of (CQC-WFF A) holds X \/ Y c= (Cn X) \/ (Cn Y)
Lm2:
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p & X |- q holds
X |- p '&' q
Lm3:
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p '&' q holds
( X |- p & X |- q )
Lm4:
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p |-| q & r |-| s holds
p '&' r |- q '&' s
Lm5:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p <==> q holds
'not' p <==> 'not' q
Lm6:
for A being QC-alphabet
for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds
p <==> q