simp_rw [subset_iff, mem_certificator, mem_disjSups]
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ s □ t ⊆ s ○ t
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ ∀ ⦃x : α⦄,
    (∃ x_1 y, IsCompl x_1 y ∧ (∀ ⦃b : α⦄, x ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, x ⊓ y = b ⊓ y → b ∈ t) →
      ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x