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