| pf |
|---|
Apply SNoL_1 with λ x0 x1 . {x2 ∈ x1|SNoLe 0 x2} = 1.
Apply set_ext with {x0 ∈ 1|SNoLe 0 x0}, 1 leaving 2 subgoals.
The subproof is completed by applying Sep_Subq with 1, λ x0 . SNoLe 0 x0. Let x0 of type ι be given.
Assume H0: x0 ∈ 1.
Apply cases_1 with x0, λ x1 . x1 ∈ Sep 1 (SNoLe 0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SepI with 1, λ x1 . SNoLe 0 x1, 0 leaving 2 subgoals.
The subproof is completed by applying In_0_1.
The subproof is completed by applying SNoLe_ref with 0.
■ |
|