begin
begin
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
begin
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 ) )