reconsider L = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1) } as closed Subset of (TOP-REAL 2) by JGRAPH_2:47;
set f = AffineMap (1,0,(1 / 2),(- (1 / 2)));
defpred S₁[ Point of (TOP-REAL 2)] means $1 `2 >= 1 - (2 * ($1 `1));
{ p where p is Point of (TOP-REAL 2) : S₁[p] } is Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
then reconsider K = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } as Subset of (TOP-REAL 2) ;
K c= the carrier of (TOP-REAL 2) ;
then A1: K c= dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) by FUNCT_2:def 1;
A2: (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: K = L by Th12;
AffineMap (1,0,(1 / 2),(- (1 / 2))) is one-to-one by JGRAPH_2:44;
then K = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) " ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: K) by A1, FUNCT_1:94;
hence { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } is closed Subset of (TOP-REAL 2) by A2, PRE_TOPC:def 6; :: thesis: verum