environ
vocabularies HIDDEN, ORDERS_2, SETFAM_1, SUBSET_1, WAYBEL_0, TARSKI, XXREAL_0, LATTICES, ORDINAL2, WAYBEL23, YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1, ORDINAL1, STRUCT_0, XBOOLE_0, PRE_TOPC, RLVECT_3, RCOMP_1, WAYBEL_3, FINSET_1, EQREL_1, ZFMISC_1, FUNCT_1, RELAT_1, WAYBEL11, YELLOW_9, WAYBEL19, PRELAMB, CANTOR_1, PROB_1, DIRAF, LATTICE3, RELAT_2, CARD_FIL, REWRITE1, PARTFUN1, FINSEQ_3, FINSEQ_1, ORDINAL4, WAYBEL_9, WELLORD1, CAT_1, WAYBEL31;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, DOMAIN_1, FINSEQ_2, FINSEQ_3, ORDINAL1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19, WAYBEL23;
definitions TARSKI, YELLOW_0, WAYBEL_8;
theorems TARSKI, SETFAM_1, SUBSET_1, FINSET_1, RELSET_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_5, CARD_1, CARD_4, WELLORD2, T_0TOPSP, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_8, YELLOW_9, YELLOW12, YELLOW15, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_7, WAYBEL_8, WAYBEL11, WAYBEL14, WAYBEL19, WAYBEL23, WAYBEL30, WAYBEL13, WSIERP_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, CARD_2;
schemes ORDINAL1, FUNCT_2, PRE_CIRC, CLASSES1, FRAENKEL, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_3, WAYBEL_4, WAYBEL_8, WAYBEL14, YELLOW_9, YELLOW11, WAYBEL19, WAYBEL23, YELLOW15, WAYBEL25, WAYBEL30, ORDINAL1, PRE_TOPC;
constructors HIDDEN, DOMAIN_1, NAT_1, FINSEQ_3, TOPS_2, CANTOR_1, WAYBEL_1, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL23, RELSET_1, WAYBEL_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities YELLOW_0, WAYBEL_8, STRUCT_0;
expansions TARSKI;
Lm1:
for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
Lm2:
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
Lm3:
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T