environ
vocabularies HIDDEN, XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, ORDERS_2, ZFMISC_1, RELAT_2, PRE_TOPC, STRUCT_0, RLVECT_3, TARSKI, SETFAM_1, XXREAL_0, REWRITE1, PRELAMB, YELLOW_9, ORDINAL1, RCOMP_1, FINSET_1, FUNCT_1, RELAT_1, ORDINAL2, YELLOW_0, LATTICES, CAT_1, ARYTM_0, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, CONNSP_2, TOPS_1, PROB_1, WAYBEL11, DIRAF, CARD_FIL, YELLOW_1, EQREL_1, COMPTS_1, WAYBEL19, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, PRE_TOPC, TOPS_1, CONNSP_2, BORSUK_1, COMPTS_1, YELLOW_0, WAYBEL_0, YELLOW_1, CANTOR_1, YELLOW_3, WAYBEL_2, YELLOW_6, YELLOW_7, WAYBEL_3, WAYBEL_9, WAYBEL11, YELLOW_9;
definitions TARSKI, PRE_TOPC, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL11, YELLOW_9, XBOOLE_0;
theorems STRUCT_0, ENUMSET1, SUBSET_1, SETFAM_1, PRE_TOPC, CANTOR_1, YELLOW_0, WAYBEL_0, FUNCT_1, RELAT_1, FUNCT_2, FINSET_1, BORSUK_1, CONNSP_2, ORDERS_2, YELLOW_2, ZFMISC_1, TARSKI, YELLOW_6, TOPS_1, TOPS_2, TEX_2, YELLOW_1, TSP_1, MSSUBFAM, WAYBEL_3, YELLOW_5, WAYBEL_7, LATTICE3, YELLOW_3, YELLOW_7, YELLOW_8, WAYBEL_9, URYSOHN1, WAYBEL11, YELLOW_9, YELLOW10, WAYBEL14, YELLOW12, XBOOLE_0, XBOOLE_1;
schemes FRAENKEL, FINSET_1, YELLOW_9, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, BORSUK_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, YELLOW12, TOPS_1, PRE_TOPC;
constructors HIDDEN, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_3, WAYBEL11, YELLOW_9, COMPTS_1, WAYBEL_2;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities LATTICE3, WAYBEL_0, WAYBEL_3, SUBSET_1, STRUCT_0;
expansions TARSKI, PRE_TOPC, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL11, XBOOLE_0;
scheme
TopInd{
F1()
-> TopLattice,
P1[
set ] } :
for
A being
Subset of
F1() st
A is
open holds
P1[
A]
provided
A1:
ex
K being
prebasis of
F1() st
for
A being
Subset of
F1() st
A in K holds
P1[
A]
and A2:
for
F being
Subset-Family of
F1() st ( for
A being
Subset of
F1() st
A in F holds
P1[
A] ) holds
P1[
union F]
and A3:
for
A1,
A2 being
Subset of
F1() st
P1[
A1] &
P1[
A2] holds
P1[
A1 /\ A2]
and A4:
P1[
[#] F1()]
Lm2:
for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
Lm3:
for T being LATTICE
for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
Lm4:
for T being LATTICE holds [#] T is property(S)