thus ( X = Y implies for e being ExtReal holds
( e in X iff e in Y ) ) ; :: thesis: ( ( for e being ExtReal holds
( e in X iff e in Y ) ) implies X = Y )
assume for e being ExtReal holds
( e in X iff e in Y ) ; :: thesis: X = Y
then ( X c= Y & Y c= X ) ;
hence X = Y ; :: thesis: verum