environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, FUNCT_1, SUBSET_1, ORDERS_2, SEQM_3, XXREAL_0, RELAT_2, LATTICE3, LATTICES, EQREL_1, WAYBEL_0, YELLOW_1, YELLOW_0, RELAT_1, CAT_1, WELLORD1, ORDINAL2, TARSKI, REWRITE1, CARD_FIL, BINOP_1, FUNCT_2, GROUP_6, YELLOW_2, LATTICE2, XBOOLEAN, ZFMISC_1, XXREAL_2, WAYBEL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2;
definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, WAYBEL_0, XBOOLE_0;
theorems ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3, RELAT_1, TARSKI, WELLORD1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes FUNCT_2, DOMAIN_1;
registrations RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, RELSET_1;
constructors HIDDEN, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, LATTICE3, WAYBEL_0, XBOOLE_0, YELLOW_2, STRUCT_0;
expansions TARSKI, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, XBOOLE_0, STRUCT_0;
Lm1:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st L2 is reflexive holds
f <= f
Lm2:
for L being non empty 1-sorted
for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
Lm3:
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g is onto
Lm4:
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g is monotone
by YELLOW_0:59;
Lm5:
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) <= b
Lm6:
for L being bounded LATTICE st L is distributive & L is complemented holds
for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
Lm7:
for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )