:: Finite Join and Finite Meet, and Dual Lattices
:: by Andrzej Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: LATTICE2:1
canceled;
theorem Th2: :: LATTICE2:2
theorem :: LATTICE2:3
canceled;
theorem :: LATTICE2:4
canceled;
theorem Th5: :: LATTICE2:5
theorem Th6: :: LATTICE2:6
theorem Th7: :: LATTICE2:7
theorem Th8: :: LATTICE2:8
theorem :: LATTICE2:9
theorem Th10: :: LATTICE2:10
theorem :: LATTICE2:11
canceled;
theorem :: LATTICE2:12
theorem Th13: :: LATTICE2:13
theorem Th14: :: LATTICE2:14
:: deftheorem Def1 defines absorbs LATTICE2:def 1 :
theorem :: LATTICE2:15
canceled;
theorem :: LATTICE2:16
canceled;
theorem Th17: :: LATTICE2:17
:: deftheorem defines .: LATTICE2:def 2 :
theorem :: LATTICE2:18
theorem :: LATTICE2:19
theorem :: LATTICE2:20
canceled;
theorem Th21: :: LATTICE2:21
theorem Th22: :: LATTICE2:22
theorem :: LATTICE2:23
canceled;
theorem Th24: :: LATTICE2:24
theorem Th25: :: LATTICE2:25
theorem Th26: :: LATTICE2:26
theorem Th27: :: LATTICE2:27
theorem Th28: :: LATTICE2:28
theorem Th29: :: LATTICE2:29
theorem Th30: :: LATTICE2:30
theorem Th31: :: LATTICE2:31
theorem Th32: :: LATTICE2:32
theorem Th33: :: LATTICE2:33
theorem Th34: :: LATTICE2:34
theorem :: LATTICE2:35
theorem Th36: :: LATTICE2:36
theorem Th37: :: LATTICE2:37
theorem :: LATTICE2:38
theorem Th39: :: LATTICE2:39
theorem Th40: :: LATTICE2:40
theorem Th41: :: LATTICE2:41
:: deftheorem defines FinJoin LATTICE2:def 3 :
:: deftheorem defines FinMeet LATTICE2:def 4 :
theorem :: LATTICE2:42
canceled;
theorem Th43: :: LATTICE2:43
theorem Th44: :: LATTICE2:44
theorem Th45: :: LATTICE2:45
theorem :: LATTICE2:46
theorem Th47: :: LATTICE2:47
theorem :: LATTICE2:48
theorem Th49: :: LATTICE2:49
theorem :: LATTICE2:50
theorem :: LATTICE2:51
theorem Th52: :: LATTICE2:52
theorem Th53: :: LATTICE2:53
theorem Th54: :: LATTICE2:54
theorem Th55: :: LATTICE2:55
theorem Th56: :: LATTICE2:56
theorem :: LATTICE2:57
theorem :: LATTICE2:58
theorem :: LATTICE2:59
theorem :: LATTICE2:60
theorem Th61: :: LATTICE2:61
theorem :: LATTICE2:62
theorem :: LATTICE2:63
theorem Th64: :: LATTICE2:64
theorem :: LATTICE2:65
theorem Th66: :: LATTICE2:66
theorem Th67: :: LATTICE2:67
theorem Th68: :: LATTICE2:68
theorem Th69: :: LATTICE2:69
theorem Th70: :: LATTICE2:70
theorem :: LATTICE2:71
theorem Th72: :: LATTICE2:72
theorem Th73: :: LATTICE2:73
theorem :: LATTICE2:74
theorem :: LATTICE2:75
theorem Th76: :: LATTICE2:76
theorem :: LATTICE2:77
theorem :: LATTICE2:78
theorem :: LATTICE2:79
theorem :: LATTICE2:80
theorem Th81: :: LATTICE2:81
theorem :: LATTICE2:82
theorem :: LATTICE2:83
:: deftheorem LATTICE2:def 5 :
canceled;
:: deftheorem Def6 defines Heyting LATTICE2:def 6 :
theorem :: LATTICE2:84
theorem :: LATTICE2:85