Apply set_ext with real, {x0 ∈ complex|CSNo_Re x0 = x0} leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: x0 ∈ real.

Apply SepI with complex, λ x1 . CSNo_Re x1 = x1, x0 leaving 2 subgoals.

Apply real_complex with x0.

The subproof is completed by applying H0.

Apply real_Re_eq with x0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: x0 ∈ {x1 ∈ complex|CSNo_Re x1 = x1}.

Apply SepE with complex, λ x1 . CSNo_Re x1 = x1, x0, x0 ∈ real leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: x0 ∈ complex.

Assume H2: CSNo_Re x0 = x0.

Apply H2 with λ x1 x2 . x1 ∈ real.

Apply complex_Re_real with x0.

The subproof is completed by applying H1.

■

Proofgold Proof