thus ( X = Y implies for r being real number holds
( r in X iff r in Y ) ) ; :: thesis: ( ( for r being real number holds
( r in X iff r in Y ) ) implies X = Y )
assume for r being real number holds
( r in X iff r in Y ) ; :: thesis: X = Y
then ( X c= Y & Y c= X ) by Def9;
hence X = Y by XBOOLE_0:def 10; :: thesis: verum