environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1, STRUCT_0, FUNCT_1, LATTICES, EQREL_1, XXREAL_2, CARD_FIL, RELAT_1, INT_2, FILTER_0, PBOOLE, LOPCLSET, ORDINAL1, FILTER_2, CAT_1, GROUP_4, OPENLATT, YELLOW11, LATTICEA, ISOMICHI, LATTICE3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, ORDINAL1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES, LATTICE2, FILTER_0, FILTER_2, SETWISEO, OPENLATT, ISOMICHI, LATTICE3;
definitions TARSKI, LATTICES, BINOP_1, STRUCT_0, XBOOLE_0, FILTER_0;
theorems TARSKI, SETFAM_1, LATTICES, PRE_TOPC, SUBSET_1, LATTICE4, FILTER_0, FUNCT_1, FUNCT_2, ZFMISC_1, LOPCLSET, RELSET_1, XBOOLE_0, XBOOLE_1, EQREL_1, ORDINAL1, ORDERS_1, FILTER_2, BOOLEALG, LATTICE3, OPENLATT;
schemes FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1, LATTICE2, FILTER_2, LATTICE3, LATTICE4;
constructors HIDDEN, BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1, LATTICE4, RELSET_1, FILTER_0, FILTER_2, OPENLATT, DOMAIN_1, BOOLEALG, ISOMICHI, LATTICE3;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES, STRUCT_0, SUBSET_1, FILTER_0, FILTER_2, OPENLATT;
expansions TARSKI, LATTICES, XBOOLE_0;
IIsPrime:
for L being Lattice holds (.L.> is prime
LemDistr:
for L being distributive Lattice
for a, x1, x2 being Element of L holds a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2)