reconsider L = { p where p is Point of : p `2 >= - (p `1 ) } as closed Subset of by JGRAPH_2:57;
set f = AffineMap 1,0 ,(1 / 2),(- (1 / 2));
defpred S1[ Point of ] means $1 `2 >= 1 - (2 * ($1 `1 ));
{ p where p is Point of : S1[p] } is Subset of
from JGRAPH_2:sch 1();
then reconsider K = { p where p is Point of : p `2 >= 1 - (2 * (p `1 )) } as Subset of ;
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 Th16;
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 : p `2 >= 1 - (2 * (p `1 )) } is closed Subset of
by A2, PRE_TOPC:def 12; verum