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 `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & 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 `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & 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 A1: ( K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0. (TOP-REAL 2) ) } & 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) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) ) & 1.REAL 2 <> 0. (TOP-REAL 2) ) by Th13, REVROT_1:19, XX;
then A2: 1.REAL 2 in K0a by A1;
A3: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 10 ;
A4: K0a c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K0a or x in D )
assume x in K0a ; :: thesis: x in D
then consider p8 being Point of (TOP-REAL 2) such that
A5: ( x = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) by A1;
A6: D = (D ` ) `
.= NonZero (TOP-REAL 2) by A1, SUBSET_1:def 5 ;
not x in {(0. (TOP-REAL 2))} by A5, TARSKI:def 1;
hence x in D by A5, A6, XBOOLE_0:def 5; :: thesis: verum

end;

hence K0a is non empty Subset of ((TOP-REAL 2) | D) by A2, A3; :: thesis: K0a is non empty Subset of (TOP-REAL 2)
thus K0a is non empty Subset of (TOP-REAL 2) by A2, A4, XBOOLE_1:1; :: thesis: verum