set J0 = NonZero (TOP-REAL 2);
defpred S₁[ Point of ] means $1 `2 <= 0 ;
set I1 = { p where p is Point of : ( S<sub>1</sub>[p] & p <> 0. (TOP-REAL 2) ) } ;
let B0 be Subset of ; :: thesis: for K0 being Subset of st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds
K0 is closed
let K0 be Subset of ; :: thesis: ( B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } implies K0 is closed )
reconsider K1 = { p7 where p7 is Point of : S₁[p7] } as Subset of from JGRAPH_2:sch 1();
A1: { p where p is Point of : ( S₁[p] & p <> 0. (TOP-REAL 2) ) } = { p7 where p7 is Point of : S₁[p7] } /\ (NonZero (TOP-REAL 2)) from JGRAPH_3:sch 2();
assume ( B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of : ( S₁[p] & p <> 0. (TOP-REAL 2) ) } ) ; :: thesis: K0 is closed
then ( K1 is closed & K0 = K1 /\ ([#] ((TOP-REAL 2) | B0)) ) by A1, JORDAN6:9, PRE_TOPC:def 10;
hence K0 is closed by PRE_TOPC:43; :: thesis: verum