simp at *
case intro
rel_sub : ∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ
rel_uniq : ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False
case intro
rel_sub : True
rel_uniq : ∀ (x : ℝ), ∃! y, y ^ 2 = x
⊢ False