environ
vocabularies HIDDEN, ARYTM_3, CARD_3, EQREL_1, FINSEQ_1, FINSET_1, FINSUB_1, FUNCT_1, RELAT_1, SETFAM_1, SIMPLEX0, SRINGS_1, SUBSET_1, TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, TEX_1, PRE_TOPC, RCOMP_1, STRUCT_0, FUNCT_2, SRINGS_4, NAT_1, XCMPLX_0, FINSEQ_2, ORDINAL4, XXREAL_0, SRINGS_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, EQREL_1, SETFAM_1, FINSET_1, CARD_3, ZFMISC_1, FINSUB_1, FUNCT_1, SIMPLEX0, CARD_1, STRUCT_0, PRE_TOPC, BINOP_1, TEX_1, ENUMSET1, ORDINAL1, RELAT_1, RELSET_1, FUNCT_2, XCMPLX_0, XXREAL_0, SRINGS_1, FINSEQ_1, FINSEQ_2, SRINGS_3;
definitions TARSKI, XBOOLE_0, EQREL_1, FINSUB_1, SRINGS_1;
theorems EQREL_1, FINSEQ_1, FINSUB_1, FUNCT_2, SETFAM_1, TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, PRE_TOPC, STRUCT_0, PRVECT_3, ENUMSET1, CARD_3, FUNCT_1, RELAT_1, SUBSET_1, PARTFUN1, CARD_1, SRINGS_1, SRINGS_2, FUNCT_5, FUNCT_6, NAT_1, FINSET_1, XCMPLX_1, FINSEQ_3, FINSEQ_2, BINOP_1, FINSEQ_5, SRINGS_3, WAYBEL12;
schemes FUNCT_1, FRAENKEL, FINSEQ_1, NAT_1, XBOOLE_0;
registrations FINSET_1, RELAT_1, RELSET_1, SIMPLEX0, SUBSET_1, COHSP_1, ORDINAL1, ZFMISC_1, STRUCT_0, SRINGS_1, CARD_3, EQREL_1, FINSEQ_1, FUNCT_1, NAT_1, CARD_1, PRE_TOPC, FUNCT_2, XCMPLX_0, XXREAL_0, FINSEQ_2, SRINGS_3, SRINGS_2, XBOOLE_0, AOFA_000;
constructors HIDDEN, COHSP_1, SRINGS_1, TEX_1, TOPREALB, SRINGS_3;
requirements HIDDEN, BOOLE, NUMERALS, SUBSET;
equalities CARD_3, TEX_1, XBOOLE_0, SETFAM_1;
expansions FINSUB_1, XBOOLE_0, TARSKI, SRINGS_1, SETFAM_1;
Thm01:
for X1, X2, X3, X4 being set holds
( ((X1 /\ X4) \ (X2 \/ X3)) /\ (X1 \ ((X2 \/ X3) \/ X4)) is empty & ((X1 /\ X4) \ (X2 \/ X3)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty & (X1 \ ((X2 \/ X3) \/ X4)) /\ (((X1 /\ X3) /\ X4) \ X2) is empty )
theorem Thm02:
for
X1,
X2,
X3,
X4 being
set holds
(X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)
Lm1:
for X1, X2, X3, X4 being set holds X1 \ (X2 \/ X3) c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
Lm2:
for X1, X2, X3, X4 being set holds (X1 /\ X4) \ X2 c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
Lm3:
for X1, X2, X3, X4 being set holds ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2
theorem Thm03:
for
X1,
X2,
X3,
X4 being
set holds
(X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
theorem Thm04:
for
X1,
X2,
X3,
X4 being
set holds
(X1 \ X2) \ (X3 \ X4) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
Thm08:
for X, Y being set
for S being with_empty_element Subset-Family of X
for f being Function of X,Y holds f .: S is with_empty_element Subset-Family of Y
Thm14:
for X being set
for S being cup-closed cap-closed with_empty_element Subset-Family of X holds
( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed )
Thm15:
for T being non empty TopSpace holds
( capOpCl T is with_empty_element & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed )
Thm22:
product <*{}*> is empty
Thm37:
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed
:: { O1 \ O2 : O1 is open, O2 is open} is semiring of sets