have : bᶜᶜ = bᶜᶜ ⊔ ⊥ := by exact (sup_bot_eq _).symm
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥