no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : K
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subfield K) (_ : s ∈ S), ↑s
simp [mem_sSup_of_directedOn Sne hS]