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:46;
set f = AffineMap (1,0,(1 / 2),(1 / 2));
defpred S₁[ Point of (TOP-REAL 2)] means $1 `2 <= (2 * ($1 `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 <= (2 * (p `1)) - 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 Th10;
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 <= (2 * (p `1)) - 1 } is closed Subset of (TOP-REAL 2) by A2, PRE_TOPC:def 6; :: thesis: verum