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 >= 1 - (2 * (p `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 >= 1 - (2 * (p `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 object ; :: 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 object 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 6;
consider p being Point of (TOP-REAL 2) such that
A5: y = p and
A6: p `2 >= 1 - (2 * (p `1)) by A1, A3;
set b = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p;
(1 / 2) * (p `2) >= (1 / 2) * (1 - (2 * (p `1))) by A6, XREAL_1:64;
then A7: ((1 / 2) * (p `2)) + (- (1 / 2)) >= ((1 / 2) - (p `1)) + (- (1 / 2)) by XREAL_1:6;
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 ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `1 = (1 * (p `1)) + 0 by EUCLID:52;
then ((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `2 >= - (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . p) `1) by A8, A7, EUCLID:52;
hence x in T by A2, A4, A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S )
assume A9: x in T ; :: thesis: x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S
then A10: 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 object such that
A11: y in dom (AffineMap (1,0,(1 / 2),(- (1 / 2)))) and
A12: x = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y by A9, FUNCT_1:def 3;
reconsider y = y as Point of (TOP-REAL 2) by A11;
set b = (AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y;
A13: (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:52;
then 2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2) >= 2 * (- (y `1)) by A10, A12, XREAL_1:64;
then A14: (2 * (((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2)) + 1 >= (2 * (- (y `1))) + 1 by XREAL_1:6;
((AffineMap (1,0,(1 / 2),(- (1 / 2)))) . y) `2 = ((1 / 2) * (y `2)) + (- (1 / 2)) by A13, EUCLID:52;
then y `2 >= 1 - (2 * (y `1)) by A14;
then y in S by A1;
hence x in (AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S by A11, A12, FUNCT_1:def 6; :: thesis: verum

end;

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