A1: 1.REAL 2 <> 0. (TOP-REAL 2) by Lm1, REVROT_1:19;
let K0a be set ; :: thesis: for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds
( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} implies ( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) ) )
assume that
A2: K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } and
A3: D ` = {(0. (TOP-REAL 2))} ; :: thesis: ( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )
( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1) ) ) by Th5;
then A4: 1.REAL 2 in K0a by A2, A1;
A5: K0a c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K0a or x in D )
A6: D = (D `) `
.= NonZero (TOP-REAL 2) by A3, SUBSET_1:def 4 ;
assume x in K0a ; :: thesis: x in D
then A7: ex p8 being Point of (TOP-REAL 2) st
( x = p8 & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) by A2;
then not x in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence x in D by A7, A6, XBOOLE_0:def 5; :: thesis: verum

end;

the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 5 ;
hence K0a is non empty Subset of ((TOP-REAL 2) | D) by A4, A5; :: thesis: K0a is non empty Subset of (TOP-REAL 2)
thus K0a is non empty Subset of (TOP-REAL 2) by A4, A5, XBOOLE_1:1; :: thesis: verum