:: Algebraic Lattices
:: by Robert Milewski
::
:: Received December 1, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :
theorem :: WAYBEL_8:1
theorem :: WAYBEL_8:2
theorem :: WAYBEL_8:3
:: deftheorem defines compactbelow WAYBEL_8:def 2 :
theorem Th4: :: WAYBEL_8:4
theorem Th5: :: WAYBEL_8:5
theorem Th6: :: WAYBEL_8:6
:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :
:: deftheorem Def4 defines algebraic WAYBEL_8:def 4 :
theorem Th7: :: WAYBEL_8:7
:: deftheorem Def5 defines arithmetic WAYBEL_8:def 5 :
theorem Th8: :: WAYBEL_8:8
theorem Th9: :: WAYBEL_8:9
theorem Th10: :: WAYBEL_8:10
theorem :: WAYBEL_8:11
theorem Th12: :: WAYBEL_8:12
theorem Th13: :: WAYBEL_8:13
theorem Th14: :: WAYBEL_8:14
theorem Th15: :: WAYBEL_8:15
theorem Th16: :: WAYBEL_8:16
theorem Th17: :: WAYBEL_8:17
theorem Th18: :: WAYBEL_8:18
theorem :: WAYBEL_8:19
canceled;
theorem :: WAYBEL_8:20
canceled;
theorem :: WAYBEL_8:21
theorem Th22: :: WAYBEL_8:22
theorem :: WAYBEL_8:23
theorem :: WAYBEL_8:24
theorem Th25: :: WAYBEL_8:25
theorem :: WAYBEL_8:26
theorem :: WAYBEL_8:27
theorem Th28: :: WAYBEL_8:28
theorem Th29: :: WAYBEL_8:29
theorem Th30: :: WAYBEL_8:30
theorem Th31: :: WAYBEL_8:31
theorem :: WAYBEL_8:32
theorem Th33: :: WAYBEL_8:33