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