begin
:: deftheorem Def1 defines join-Associative ROBBINS3:def 1 :
:: deftheorem Def2 defines meet-Associative ROBBINS3:def 2 :
:: deftheorem Def3 defines meet-Absorbing ROBBINS3:def 3 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
theorem Th6:
theorem Th7:
begin
:: deftheorem defines TrivLattRelStr ROBBINS3:def 4 :
theorem
Lm1:
TrivLattRelStr is Lattice-like
;
begin
:: deftheorem defines TrivCLRelStr ROBBINS3:def 5 :
:: deftheorem Def6 defines involutive ROBBINS3:def 6 :
:: deftheorem Def7 defines with_Top ROBBINS3:def 7 :
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem defines RelAugmentation ROBBINS3:def 8 :
:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :
:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def 10 :
:: deftheorem Def11 defines naturally_inf-generated ROBBINS3:def 11 :
theorem Th22:
theorem Th23:
begin
definition
let R be
OrthoLattStr ;
mode CLatAugmentation of
R -> OrthoLattRelStr means :
Def12:
OrthoLattStr(# the
carrier of
it,the
L_join of
it,the
L_meet of
it,the
Compl of
it #)
= OrthoLattStr(# the
carrier of
R,the
L_join of
R,the
L_meet of
R,the
Compl of
R #);
existence
ex b1 being OrthoLattRelStr st OrthoLattStr(# the carrier of b1,the L_join of b1,the L_meet of b1,the Compl of b1 #) = OrthoLattStr(# the carrier of R,the L_join of R,the L_meet of R,the Compl of R #)
end;
:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
theorem Th30: