environ
vocabularies HIDDEN, CONLAT_1, STRUCT_0, QC_LANG1, SUBSET_1, LATTICES, XXREAL_2, PBOOLE, EQREL_1, XBOOLE_0, SETFAM_1, FUNCT_1, TARSKI, CAT_1, LATTICE3, ZFMISC_1, RELAT_1, FUNCT_3, LATTICE6, REWRITE1, GROUP_6, WELLORD1, FUNCT_2, MCART_1, FILTER_1, XXREAL_0, ORDERS_2, CONLAT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, XTUPLE_0, MCART_1, FUNCT_1, DOMAIN_1, RELSET_1, ORDERS_2, STRUCT_0, LATTICE2, LATTICE3, LATTICE6, PARTFUN1, FUNCT_2, LATTICES, LATTICE4, CONLAT_1;
definitions TARSKI, LATTICE3, VECTSP_8, LATTICE6, FUNCT_1, XBOOLE_0;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, LATTICE4, LATTICES, LATTICE3, SETFAM_1, FUNCT_2, FILTER_1, LATTICE2, ORDERS_2, CONLAT_1, XTUPLE_0;
schemes FUNCT_2;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2, LATTICE3, CONLAT_1, RELSET_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, LATTICE2, LATTICE4, CONLAT_1, LATTICE6, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICE3, XBOOLE_0, SUBSET_1;
expansions LATTICE3, LATTICE6, FUNCT_1, XBOOLE_0;
Lm1:
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
Lm2:
for L1, L2 being complete Lattice
for f being Function of the carrier of L1, the carrier of L2 st f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
Lm3:
for C being FormalContext
for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty