defpred S₁[ Point of (TOP-REAL 2)] means $1 `2 <= 0 ;
let sn be Real; :: thesis: for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= sn * |.p.| & p `2 <= 0 ) } holds
K03 is closed
let K003 be Subset of (TOP-REAL 2); :: thesis: ( K003 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= sn * |.p.| & p `2 <= 0 ) } implies K003 is closed )
assume A1: K003 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= sn * |.p.| & p `2 <= 0 ) } ; :: thesis: K003 is closed
reconsider KX = { p where p is Point of (TOP-REAL 2) : S<sub>1</sub>[p] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
defpred S<sub>2</sub>[ Point of (TOP-REAL 2)] means $1 `1 <= sn * |.$1.|;
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: { p where p is Point of (TOP-REAL 2) : ( S₂[p] & S₁[p] ) } = { p7 where p7 is Point of (TOP-REAL 2) : S₂[p7] } /\ { p1 where p1 is Point of (TOP-REAL 2) : S₁[p1] } from DOMAIN_1:sch 10();
( K1 is closed & KX is closed ) by Lm10, JORDAN6:8;
hence K003 is closed by A1, A2, TOPS_1:8; :: thesis: verum