begin
:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def 1 :
theorem
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem
theorem
theorem
theorem
begin
theorem Th24:
:: deftheorem Def2 defines antitone WAYBEL21:def 2 :
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
:: deftheorem Def3 defines Embedding WAYBEL21:def 3 :
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
begin
theorem Th45:
theorem Th46:
:: deftheorem defines lim_infs-preserving WAYBEL21:def 4 :
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem