environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PBOOLE, REAL_1, STRUCT_0, MSUALG_5, EQREL_1, RELAT_1, FUNCT_1, MSUALG_4, TARSKI, ZFMISC_1, XXREAL_2, SUBSET_1, LATTICES, CLOSURE2, SETFAM_1, FUNCT_4, REWRITE1, LATTICE3, MSSUBFAM, NAT_LAT, REALSET1, XXREAL_0, XXREAL_1, REAL_LAT, BINOP_1, SUPINF_1, ORDINAL2, ARYTM_1, CARD_1, ARYTM_3, MSUALG_7, SETLIM_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SUPINF_1, ORDINAL1, FUNCT_7, XXREAL_0, REAL_1, XXREAL_2, XCMPLX_0, XREAL_0, STRUCT_0, RELSET_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, NUMBERS, RCOMP_1, EQREL_1, BINOP_1, REALSET1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, MSUALG_3, MSUALG_4, MSUALG_5, SETFAM_1, MSSUBFAM, CLOSURE2;
definitions TARSKI, LATTICE3, XXREAL_2;
theorems TARSKI, PBOOLE, MSSUBFAM, LATTICE3, VECTSP_8, MSUALG_4, MSUALG_5, ZFMISC_1, SETFAM_1, EQREL_1, LATTICES, NAT_LAT, FUNCT_1, REAL_LAT, FUNCT_2, RCOMP_1, MSUALG_3, CLOSURE2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NUMBERS, RELAT_1, XXREAL_2, XREAL_0;
schemes DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2, ORDINAL1;
constructors HIDDEN, BINOP_1, REAL_1, SQUARE_1, SUPINF_1, RCOMP_1, REALSET1, MSSUBFAM, REAL_LAT, LATTICE3, MSUALG_3, MSUALG_5, CLOSURE2, XXREAL_2, RELSET_1, FUNCT_7;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, REALSET1;
expansions TARSKI, LATTICE3, XXREAL_2;
definition
let r1,
r2 be
Real;
assume A1:
r1 <= r2
;
existence
ex b1 being strict Lattice st
( the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] )
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = [.r1,r2.] & the L_join of b1 = maxreal || [.r1,r2.] & the L_meet of b1 = minreal || [.r1,r2.] & the carrier of b2 = [.r1,r2.] & the L_join of b2 = maxreal || [.r1,r2.] & the L_meet of b2 = minreal || [.r1,r2.] holds
b1 = b2
;
end;
reconsider jj = 1 as Real ;
reconsider jd = 1 / 2 as Real ;