let X1, X2 be Subset of [:I[01],I[01]:]; ( ( 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) ) ) ) & ( 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) ) ) ) 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) ) )
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) ) )
; X1 = X2
X1 = X2
hence
X1 = X2
; verum