environ
vocabularies HIDDEN, ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, TARSKI, REWRITE1, WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, EQREL_1, RELAT_2, FINSET_1, ORDINAL2, YELLOW_0, ZFMISC_1, STRUCT_0, CARD_1, RELAT_1, CARD_FIL, WAYBEL_9, RCOMP_1, NATTRA_1, PRE_TOPC, T_0TOPSP, CONNSP_2, TOPS_1, FUNCT_1, YELLOW_6, SEQM_3, CLASSES2, CLASSES1, YELLOW_2, PROB_1, WAYBEL_3, ORDINAL1, CARD_3, PBOOLE, WAYBEL_5, FUNCT_6, RLVECT_2, WAYBEL_6, RLVECT_3, YELLOW_8, WAYBEL11;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, WAYBEL_6, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2, CARD_3, PRALG_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_6, WAYBEL_9, YELLOW_8;
definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, TOPS_2, YELLOW_8, WAYBEL_6;
theorems TSP_1, WAYBEL_0, YELLOW_0, TARSKI, SUBSET_1, TOPS_1, YELLOW_2, SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1, ORDERS_2, LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7, YELLOW_1, YELLOW_3, WAYBEL_3, FUNCT_1, FUNCT_2, YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1, RELAT_1, WAYBEL_4, YELLOW_8, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes RELSET_1, DOMAIN_1, FRAENKEL, PBOOLE, XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, TDLAT_3, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_5, WAYBEL_9, RELSET_1, TOPS_1;
constructors HIDDEN, DOMAIN_1, CLASSES1, CLASSES2, TOPS_1, CONNSP_2, TDLAT_3, T_0TOPSP, CANTOR_1, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_9, YELLOW_8, RELSET_1, TOPS_2, WAYBEL_2, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities STRUCT_0, SUBSET_1, WAYBEL_0, YELLOW_6, WAYBEL_3, BINOP_1;
expansions XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3;
Lm1:
for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
Lm2:
for T being non empty reflexive TopRelStr holds [#] T is property(S)
defpred S1[ set ] means verum;
Lm3:
for T1, T2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like holds
T2 is TopSpace-like
;
Lm4:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being strict net of S1 holds N is strict net of S2
;
Lm5:
for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
Lm6:
for T1, T2 being non empty 1-sorted
for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
Lm7:
for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
Lm8:
for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
Convergence T1 = Convergence T2
Lm9:
for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE holds
R2 is LATTICE
Lm10:
for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
by Lm1;
Lm11:
for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
by Lm1;
Lm12:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "\/" (D,R1) = "\/" (D,R2)
Lm13:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "/\" (D,R1) = "/\" (D,R2)
Lm14:
for R1, R2 being non empty reflexive RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
Lm15:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
Lm16:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
Lm17:
for R1, R2 being non empty reflexive RelStr
for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
Lm18:
for R1, R2 being non empty reflexive RelStr
for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
Lm19:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 c= Scott-Convergence R2
Lm20:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 = Scott-Convergence R2
by Lm19;
Lm21:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
sigma R1 = sigma R2
Lm22:
for R1, R2 being LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete holds
R2 is complete
Lm23:
for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous holds
R2 is continuous