set f = AffineMap 1,0 ,(1 / 2),(1 / 2);
set A = 1;
set B = 0 ;
set C = 1 / 2;
set D = 1 / 2;
let S, T be Subset of (TOP-REAL 2); :: thesis: ( S = { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= p `1 } implies (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S = T )
assume that
A1: S = { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } and
A2: T = { p where p is Point of (TOP-REAL 2) : p `2 >= p `1 } ; :: thesis: (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S = T
(AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S = T

proof

thus (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S c= T :: according to XBOOLE_0:def 10 :: thesis: T c= (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S or x in T )
assume x in (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S ; :: thesis: x in T
then consider y being set such that
y in dom (AffineMap 1,0 ,(1 / 2),(1 / 2)) and
A3: y in S and
A4: x = (AffineMap 1,0 ,(1 / 2),(1 / 2)) . y by FUNCT_1:def 12;
consider p being Point of (TOP-REAL 2) such that
A5: y = p and
A6: p `2 >= (2 * (p `1 )) - 1 by A1, A3;
A7: (1 / 2) * (p `2 ) >= (1 / 2) * ((2 * (p `1 )) - 1) by A6, XREAL_1:66;
set b = (AffineMap 1,0 ,(1 / 2),(1 / 2)) . p;
A8: (AffineMap 1,0 ,(1 / 2),(1 / 2)) . p = |[((1 * (p `1 )) + 0 ),(((1 / 2) * (p `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then A9: ((AffineMap 1,0 ,(1 / 2),(1 / 2)) . p) `1 = (1 * (p `1 )) + 0 by EUCLID:56;
((AffineMap 1,0 ,(1 / 2),(1 / 2)) . p) `2 = ((1 / 2) * (p `2 )) + (1 / 2) by A8, EUCLID:56;
then ((AffineMap 1,0 ,(1 / 2),(1 / 2)) . p) `2 >= ((p `1 ) - (1 / 2)) + (1 / 2) by A7, XREAL_1:8;
hence x in T by A2, A4, A5, A9; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S )
assume A10: x in T ; :: thesis: x in (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S
then A11: ex p being Point of (TOP-REAL 2) st
( x = p & p `2 >= p `1 ) by A2;
AffineMap 1,0 ,(1 / 2),(1 / 2) is onto by JORDAN1K:36;
then rng (AffineMap 1,0 ,(1 / 2),(1 / 2)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
then consider y being set such that
A12: y in dom (AffineMap 1,0 ,(1 / 2),(1 / 2)) and
A13: x = (AffineMap 1,0 ,(1 / 2),(1 / 2)) . y by A10, FUNCT_1:def 5;
reconsider y = y as Point of (TOP-REAL 2) by A12;
set b = (AffineMap 1,0 ,(1 / 2),(1 / 2)) . y;
A14: (AffineMap 1,0 ,(1 / 2),(1 / 2)) . y = |[((1 * (y `1 )) + 0 ),(((1 / 2) * (y `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then ((AffineMap 1,0 ,(1 / 2),(1 / 2)) . y) `1 = y `1 by EUCLID:56;
then 2 * (((AffineMap 1,0 ,(1 / 2),(1 / 2)) . y) `2 ) >= 2 * (y `1 ) by A11, A13, XREAL_1:66;
then A15: (2 * (((AffineMap 1,0 ,(1 / 2),(1 / 2)) . y) `2 )) - 1 >= (2 * (y `1 )) - 1 by XREAL_1:11;
((AffineMap 1,0 ,(1 / 2),(1 / 2)) . y) `2 = ((1 / 2) * (y `2 )) + (1 / 2) by A14, EUCLID:56;
then y in S by A1, A15;
hence x in (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S by A12, A13, FUNCT_1:def 12; :: thesis: verum

end;

hence (AffineMap 1,0 ,(1 / 2),(1 / 2)) .: S = T ; :: thesis: verum