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:57;
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 Th17;
AffineMap 1,0 ,(1 / 2),(- (1 / 2)) is one-to-one by JGRAPH_2:54;
then K = (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) " ((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: K) by A1, FUNCT_1:164;
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 12; :: thesis: verum