Proof of Theorem womaon
Step | Hyp | Ref
| Expression |
1 | | lea 160 |
. . 3
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) ≤ a |
2 | | lear 161 |
. . . 4
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) ≤ (a⊥ ∪ (a ∩ (a⊥ ∪ b))) |
3 | | leo 158 |
. . . . 5
a⊥ ≤ (a⊥ ∪ b) |
4 | | lear 161 |
. . . . 5
(a ∩ (a⊥ ∪ b)) ≤ (a⊥ ∪ b) |
5 | 3, 4 | lel2or 170 |
. . . 4
(a⊥ ∪ (a ∩ (a⊥ ∪ b))) ≤ (a⊥ ∪ b) |
6 | 2, 5 | letr 137 |
. . 3
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) ≤ (a⊥ ∪ b) |
7 | 1, 6 | ler2an 173 |
. 2
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) ≤ (a
∩ (a⊥ ∪ b)) |
8 | | lea 160 |
. . 3
(a ∩ (a⊥ ∪ b)) ≤ a |
9 | | leor 159 |
. . 3
(a ∩ (a⊥ ∪ b)) ≤ (a⊥ ∪ (a ∩ (a⊥ ∪ b))) |
10 | 8, 9 | ler2an 173 |
. 2
(a ∩ (a⊥ ∪ b)) ≤ (a
∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) |
11 | 7, 10 | lebi 145 |
1
(a ∩ (a⊥ ∪ (a ∩ (a⊥ ∪ b)))) = (a ∩
(a⊥ ∪ b)) |