F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
⊢ S ≤ ↑⊥ ↔ S ⊆ ↑⊥
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
⊢ adjoin F S = ⊥ ↔ S ⊆ ↑⊥
rw [eq_bot_iff, adjoin_le_iff]
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
⊢ S ≤ ↑⊥ ↔ S ⊆ ↑⊥
rfl