environ
vocabularies HIDDEN, XBOOLE_0, LATTICES, SUBSET_1, EQREL_1, SHEFFER1, ROBBINS1, OPOSET_1, QMAX_1, FUNCT_1, WAYBEL_0, XXREAL_0, LATTICE3, STRUCT_0, ORDERS_2, BINOP_1, RELAT_1, FUNCT_5, ZFMISC_1, RELAT_2, FILTER_1, ORDERS_1, PBOOLE, TARSKI, YELLOW_0, WAYBEL_1, ROBBINS3, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1, RELAT_2, FUNCT_2, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICE3, LATTICES, ORDERS_1, ORDERS_2, FILTER_1, ROBBINS1, QMAX_1, OPOSET_1, WAYBEL_0, WAYBEL_1, YELLOW_0, SHEFFER1, PARTIT_2;
definitions LATTICES, RELAT_2, TARSKI, STRUCT_0;
theorems ZFMISC_1, STRUCT_0, LATTICE3, RELAT_1, FILTER_1, LATTICES, OPOSET_1, ORDERS_1, ROBBINS1, PARTFUN1, RELAT_2, YELLOW_0, ORDERS_2, WAYBEL_9, WAYBEL_1, FUNCT_2, YELLOW_7, SHEFFER1, PARTIT_2;
schemes ;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, LATTICES, YELLOW_0, YELLOW_1, ROBBINS1, OPOSET_1, SHEFFER1, PARTIT_2, CARD_1;
constructors HIDDEN, BINOP_1, REALSET2, LATTICE3, WAYBEL_1, YELLOW_6, OPOSET_1, SHEFFER1, FUNCT_5, RELSET_1, PARTIT_2;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities LATTICES, ORDINAL1;
expansions LATTICES, RELAT_2, STRUCT_0;
Lm1:
TrivLattRelStr is Lattice-like
;
theorem
for
K,
L being non
empty LattStr st
LattStr(# the
carrier of
K, the
L_join of
K, the
L_meet of
K #)
= LattStr(# the
carrier of
L, the
L_join of
L, the
L_meet of
L #) &
K is
Lattice-like holds
L is
Lattice-like by Th9, Th10, Th11, Th12, Th13, Th14;