begin
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
begin
theorem Th18:
theorem Th19:
theorem Th20:
:: deftheorem defines sup WAYBEL_2:def 1 :
definition
let L be non
empty RelStr ;
let J be
set ;
let f be
Function of
J,the
carrier of
L;
func FinSups f -> prenet of
means :
Def2:
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) &
it = NetStr(#
(Fin J),
(RelIncl (Fin J)),
g #) );
existence
ex b1 being prenet of 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 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;
:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :
theorem
:: deftheorem Def3 defines "/\" WAYBEL_2:def 3 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
begin
definition
let L be non
empty RelStr ;
func inf_op L -> Function of
[:L,L:],
L means :
Def4:
for
x,
y being
Element of holds
it . x,
y = x "/\" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of holds b1 . x,y = x "/\" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of holds b1 . x,y = x "/\" y ) & ( for x, y being Element of holds b2 . x,y = x "/\" y ) holds
b1 = b2
end;
:: deftheorem Def4 defines inf_op WAYBEL_2:def 4 :
theorem Th31:
theorem Th32:
theorem Th33:
definition
let L be non
empty RelStr ;
func sup_op L -> Function of
[:L,L:],
L means :
Def5:
for
x,
y being
Element of holds
it . x,
y = x "\/" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of holds b1 . x,y = x "\/" y
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of holds b1 . x,y = x "\/" y ) & ( for x, y being Element of holds b2 . x,y = x "\/" y ) holds
b1 = b2
end;
:: deftheorem Def5 defines sup_op WAYBEL_2:def 5 :
theorem Th34:
theorem Th35:
theorem
begin
:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def 6 :
:: deftheorem Def7 defines meet-continuous WAYBEL_2:def 7 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem
theorem Th53:
theorem Th54:
theorem
Lm1:
for L being meet-continuous Semilattice
for x being Element of holds x "/\" is directed-sups-preserving
theorem Th56: