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.REAL 2 ) } ;
set J0 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)};
let B0 be Subset of (TOP-REAL 2); :: thesis: for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0.REAL 2 ) } holds
K0 is closed
let K0 be Subset of ((TOP-REAL 2) | B0); :: thesis: ( B0 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0.REAL 2 ) } implies K0 is closed )
assume A1: ( B0 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & K0 = { p where p is Point of (TOP-REAL 2) : ( S₁[p] & p <> 0.REAL 2 ) } ) ; :: thesis: 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();
A2: K1 is closed by JORDAN6:8;
{ p where p is Point of (TOP-REAL 2) : ( S₁[p] & p <> 0.REAL 2 ) } = { p7 where p7 is Point of (TOP-REAL 2) : S₁[p7] } /\ (the carrier of (TOP-REAL 2) \ {(0.REAL 2)}) from JGRAPH_3:sch 2();
then K0 = K1 /\ ([#] ((TOP-REAL 2) | B0)) by A1, PRE_TOPC:def 10;
hence K0 is closed by A2, PRE_TOPC:43; :: thesis: verum