environ
vocabularies HIDDEN, ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, RELAT_2, FINSET_1, LATTICE3, TARSKI, LATTICES, YELLOW_0, STRUCT_0, EQREL_1, CAT_1, FUNCT_1, RELAT_1, SEQM_3, FUNCOP_1, SETFAM_1, ORDINAL2, CARD_FIL, REWRITE1, ZFMISC_1, ORDERS_1, CARD_1, TREES_2, WAYBEL_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, RELAT_2, FINSET_1, FUNCT_1, RELSET_1, ORDINAL1, NUMBERS, FUNCT_2, FUNCOP_1, ORDERS_1, DOMAIN_1, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_2, ORDERS_3;
definitions TARSKI, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_3, XBOOLE_0;
theorems TARSKI, ZFMISC_1, ORDERS_2, LATTICE3, FUNCT_2, FUNCOP_1, YELLOW_0, RELAT_2, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes FINSET_1, XBOOLE_0;
registrations XBOOLE_0, RELSET_1, FINSET_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, SUBSET_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, LATTICE3, YELLOW_0, ORDERS_3, REALSET1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE;
equalities STRUCT_0, LATTICE3;
expansions TARSKI, LATTICE3, YELLOW_0, ORDERS_3;
definition
let L be non
empty RelStr ;
let X be
Subset of
L;
set D =
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1:
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } c= the
carrier of
L
correctness
coherence
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L;
by A1;
set D =
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2:
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } c= the
carrier of
L
correctness
coherence
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;
by A2;
end;
:: in our terminology. It is shown bellow.