begin
begin
definition
let L be non
empty RelStr ;
let J be
set ;
let f be
Function of
J, the
carrier of
L;
existence
ex b1 being prenet of L ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
uniqueness
for b1, b2 being prenet of L st ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
end;
begin
definition
let L be non
empty RelStr ;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "/\" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "/\" y ) holds
b1 = b2
end;
definition
let L be non
empty RelStr ;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "\/" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "\/" y ) holds
b1 = b2
end;
begin
Lm1:
for L being meet-continuous Semilattice
for x being Element of L holds x "/\" is directed-sups-preserving