:: Boolean Properties of Lattices
:: by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem defines \ BOOLEALG:def 1 :
:: deftheorem defines \+\ BOOLEALG:def 2 :
:: deftheorem Def3 defines = BOOLEALG:def 3 :
:: deftheorem Def4 defines meets BOOLEALG:def 4 :
theorem :: BOOLEALG:1
canceled;
theorem :: BOOLEALG:2
canceled;
theorem :: BOOLEALG:3
theorem :: BOOLEALG:4
theorem :: BOOLEALG:5
canceled;
theorem :: BOOLEALG:6
theorem :: BOOLEALG:7
canceled;
theorem :: BOOLEALG:8
canceled;
theorem :: BOOLEALG:9
canceled;
theorem :: BOOLEALG:10
theorem :: BOOLEALG:11
theorem :: BOOLEALG:12
Lm2:
for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X
theorem :: BOOLEALG:13
canceled;
theorem :: BOOLEALG:14
canceled;
theorem :: BOOLEALG:15
canceled;
theorem :: BOOLEALG:16
theorem :: BOOLEALG:17
canceled;
theorem :: BOOLEALG:18
canceled;
theorem :: BOOLEALG:19
canceled;
theorem :: BOOLEALG:20
canceled;
theorem :: BOOLEALG:21
canceled;
theorem :: BOOLEALG:22
theorem :: BOOLEALG:23
canceled;
theorem :: BOOLEALG:24
canceled;
theorem Th25: :: BOOLEALG:25
theorem :: BOOLEALG:26
theorem Th27: :: BOOLEALG:27
theorem :: BOOLEALG:28
theorem :: BOOLEALG:29
canceled;
theorem Th30: :: BOOLEALG:30
theorem Th31: :: BOOLEALG:31
theorem :: BOOLEALG:32
theorem :: BOOLEALG:33
theorem :: BOOLEALG:34
theorem :: BOOLEALG:35
theorem :: BOOLEALG:36
theorem :: BOOLEALG:37
theorem :: BOOLEALG:38
theorem Th39: :: BOOLEALG:39
theorem :: BOOLEALG:40
theorem :: BOOLEALG:41
theorem :: BOOLEALG:42
theorem :: BOOLEALG:43
theorem :: BOOLEALG:44
theorem :: BOOLEALG:45
theorem Th46: :: BOOLEALG:46
theorem :: BOOLEALG:47
theorem :: BOOLEALG:48
theorem :: BOOLEALG:49
theorem Th50: :: BOOLEALG:50
theorem :: BOOLEALG:51
theorem Th52: :: BOOLEALG:52
theorem Th53: :: BOOLEALG:53
theorem Th54: :: BOOLEALG:54
theorem :: BOOLEALG:55
theorem :: BOOLEALG:56
theorem :: BOOLEALG:57
theorem :: BOOLEALG:58
theorem Th59: :: BOOLEALG:59
theorem :: BOOLEALG:60
theorem Th61: :: BOOLEALG:61
theorem Th62: :: BOOLEALG:62
theorem :: BOOLEALG:63
theorem :: BOOLEALG:64
canceled;
theorem :: BOOLEALG:65
canceled;
theorem :: BOOLEALG:66
canceled;
theorem Th67: :: BOOLEALG:67
theorem :: BOOLEALG:68
theorem Th69: :: BOOLEALG:69
theorem Th70: :: BOOLEALG:70
theorem :: BOOLEALG:71
theorem :: BOOLEALG:72
theorem :: BOOLEALG:73
theorem :: BOOLEALG:74
theorem :: BOOLEALG:75
theorem :: BOOLEALG:76
theorem :: BOOLEALG:77
theorem :: BOOLEALG:78
theorem :: BOOLEALG:79
theorem :: BOOLEALG:80
theorem :: BOOLEALG:81
Lm4:
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
theorem :: BOOLEALG:82
theorem :: BOOLEALG:83
theorem Th84: :: BOOLEALG:84
theorem :: BOOLEALG:85
theorem :: BOOLEALG:86
theorem :: BOOLEALG:87
theorem :: BOOLEALG:88