begin
:: deftheorem defines TrivComplLat ROBBINS1:def 1 :
:: deftheorem defines TrivOrtLat ROBBINS1:def 2 :
:: deftheorem defines ` ROBBINS1:def 3 :
:: deftheorem defines *' ROBBINS1:def 4 :
:: deftheorem Def5 defines Robbins ROBBINS1:def 5 :
:: deftheorem Def6 defines Huntington ROBBINS1:def 6 :
:: deftheorem Def7 defines join-idempotent ROBBINS1:def 7 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def8 defines Top ROBBINS1:def 8 :
theorem Th7:
theorem Th8:
:: deftheorem Def9 defines Bot ROBBINS1:def 9 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
begin
:: deftheorem Def10 defines well-complemented ROBBINS1:def 10 :
theorem Th33:
theorem Th34:
begin
:: deftheorem Def11 defines CLatt ROBBINS1:def 11 :
theorem
theorem Th36:
begin
:: deftheorem Def12 defines Huntington ROBBINS1:def 12 :
:: deftheorem Def13 defines with_idempotent_element ROBBINS1:def 13 :
:: deftheorem defines \delta ROBBINS1:def 14 :
:: deftheorem defines Expand ROBBINS1:def 15 :
:: deftheorem defines _0 ROBBINS1:def 16 :
:: deftheorem defines Double ROBBINS1:def 17 :
:: deftheorem defines _1 ROBBINS1:def 18 :
:: deftheorem defines _2 ROBBINS1:def 19 :
:: deftheorem defines _3 ROBBINS1:def 20 :
:: deftheorem defines _4 ROBBINS1:def 21 :
theorem Th37:
theorem
theorem
theorem
theorem Th41:
theorem Th42:
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
:: deftheorem defines \beta ROBBINS1:def 22 :
theorem Th54:
theorem Th55:
theorem
begin
theorem
theorem Th58:
theorem Th59:
theorem Th60:
:: deftheorem Def23 defines de_Morgan ROBBINS1:def 23 :
theorem Th61:
theorem Th62:
theorem Th63: