begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :
begin
:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :
theorem Th3:
begin
theorem Th4:
theorem Th5:
:: deftheorem defines OSConstants OSALG_2:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
:: deftheorem Def4 defines OSCl OSALG_2:def 4 :
theorem Th12:
theorem Th13:
theorem
:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
begin
theorem Th20:
:: deftheorem defines OSbool OSALG_2:def 6 :
:: deftheorem defines OSSubSort OSALG_2:def 7 :
theorem Th21:
theorem Th22:
:: deftheorem defines OSSubSort OSALG_2:def 8 :
theorem Th23:
:: deftheorem defines @ OSALG_2:def 9 :
theorem Th24:
theorem Th25:
:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
begin
:: deftheorem OSALG_2:def 12 :
canceled;
:: deftheorem Def13 defines GenOSAlg OSALG_2:def 13 :
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
:: deftheorem Def14 defines "\/"_os OSALG_2:def 14 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
begin
:: deftheorem Def15 defines OSSub OSALG_2:def 15 :
theorem Th47:
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
func OSAlg_join U0 -> BinOp of
(OSSub U0) means :
Def16:
for
x,
y being
Element of
OSSub U0 for
U1,
U2 being
strict OSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 "\/"_os U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/"_os U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 "\/"_os U2 ) holds
b1 = b2
end;
:: deftheorem Def16 defines OSAlg_join OSALG_2:def 16 :
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
func OSAlg_meet U0 -> BinOp of
(OSSub U0) means :
Def17:
for
x,
y being
Element of
OSSub U0 for
U1,
U2 being
strict OSSubAlgebra of
U0 st
x = U1 &
y = U2 holds
it . x,
y = U1 /\ U2;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
end;
:: deftheorem Def17 defines OSAlg_meet OSALG_2:def 17 :
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
:: deftheorem defines OSSubAlLattice OSALG_2:def 18 :
theorem Th53:
theorem
theorem Th55:
theorem