environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, SUBSET_1, TARSKI, WAYBEL_0, XBOOLE_0, TREES_2, LATTICES, XXREAL_0, FINSET_1, TREES_1, CARD_1, NAT_1, ARYTM_3, ORDERS_2, RELAT_2, ORDERS_1, LATTICE3, EQREL_1, ORDINAL2, YELLOW_0, FUNCT_1, YELLOW_1, CAT_1, PBOOLE, RELAT_1, WELLORD1, COHSP_1, ZFMISC_1, LATTICE7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, CARD_1, ORDINAL1, NUMBERS, STRUCT_0, ORDERS_1, PBOOLE, XCMPLX_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_4, WAYBEL_1, WAYBEL_0, NAT_1, RELAT_2, COHSP_1, XXREAL_0;
definitions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, RELAT_2, COHSP_1;
theorems WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_4, TARSKI, FUNCT_1, FUNCT_2, ORDERS_2, WAYBEL_4, CARD_1, CARD_2, NAT_1, YELLOW_5, WAYBEL13, WAYBEL_6, RELSET_1, XBOOLE_0, XBOOLE_1, XXREAL_0, ORDINAL1, PARTFUN1;
schemes NAT_1, PBOOLE;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_2, WAYBEL11, YELLOW11, XXREAL_0, RELSET_1, ORDINAL1, XCMPLX_0, NAT_1;
constructors HIDDEN, DOMAIN_1, NAT_1, MEMBERED, COHSP_1, WAYBEL_1, YELLOW_4, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities WAYBEL_0;
expansions TARSKI, WAYBEL_0, WAYBEL_1, LATTICE3, COHSP_1;
Lm1:
for L being finite distributive LATTICE
for a being Element of L st ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
Lm2:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
;
Lm3:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
;