environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, ORDERS_2, SUBSET_1, XXREAL_0, RELAT_1, RELAT_2, REWRITE1, LATTICE3, ZFMISC_1, ORDERS_1, ARYTM_3, TARSKI, LATTICES, XXREAL_2, EQREL_1, FILTER_0, PBOOLE, ORDINAL2, FINSET_1, CAT_1, WELLORD1, YELLOW_0, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_2, RELSET_1, FINSET_1, TOLER_1, ORDERS_1, DOMAIN_1, CARD_1, STRUCT_0, LATTICES, ORDERS_2, LATTICE3;
definitions STRUCT_0, RELAT_2, ORDERS_2, LATTICE3;
theorems TARSKI, ZFMISC_1, ORDERS_2, LATTICE3, XBOOLE_0, XBOOLE_1, STRUCT_0;
schemes FINSET_1, RELSET_1;
registrations XBOOLE_0, RELSET_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3, CARD_1;
constructors HIDDEN, TOLER_1, REALSET2, LATTICE3;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities LATTICE3, WELLORD1;
expansions STRUCT_0, RELAT_2, ORDERS_2, LATTICE3;
theorem
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of
S st
ex_inf_of {x,y},
L &
"/\" (
{x,y},
L)
in the
carrier of
S holds
(
ex_inf_of {x,y},
S &
"/\" (
{x,y},
S)
= "/\" (
{x,y},
L) )
by Th63;
theorem
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of
S st
ex_sup_of {x,y},
L &
"\/" (
{x,y},
L)
in the
carrier of
S holds
(
ex_sup_of {x,y},
S &
"\/" (
{x,y},
S)
= "\/" (
{x,y},
L) )
by Th64;