let X1, X2 be Subset of [:I[01],I[01]:]; :: thesis: ( ( for x being set holds
( x in X1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in X2 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) and
A3: for x being set holds
( x in X2 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ; :: thesis: X1 = X2
X1 = X2

proof

thus X1 c= X2 :: according to XBOOLE_0:def 10 :: thesis: X2 c= X1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in X2 )
assume x in X1 ; :: thesis: x in X2
then ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) by A2;
hence x in X2 by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X2 or x in X1 )
assume x in X2 ; :: thesis: x in X1
then ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) by A3;
hence x in X1 by A2; :: thesis: verum

end;

hence X1 = X2 ; :: thesis: verum