let Y be Subset of REAL; :: thesis: ( ( for r being Real holds

( r in Y iff r in REAL ) ) iff Y = REAL )

thus ( ( for r being Real holds

( r in Y iff r in REAL ) ) implies Y = REAL ) :: thesis: ( Y = REAL implies for r being Real holds

( r in Y iff r in REAL ) )

( r in Y iff r in REAL )

let r be Real; :: thesis: ( r in Y iff r in REAL )

thus ( r in Y implies r in REAL ) ; :: thesis: ( r in REAL implies r in Y )

thus ( r in REAL implies r in Y ) by A1; :: thesis: verum

( r in Y iff r in REAL ) ) iff Y = REAL )

thus ( ( for r being Real holds

( r in Y iff r in REAL ) ) implies Y = REAL ) :: thesis: ( Y = REAL implies for r being Real holds

( r in Y iff r in REAL ) )

proof

assume A1:
Y = REAL
; :: thesis: for r being Real holds
assume
for r being Real holds

( r in Y iff r in REAL ) ; :: thesis: Y = REAL

then for y being object holds

( y in Y iff y in REAL ) ;

hence Y = REAL by TARSKI:2; :: thesis: verum

end;( r in Y iff r in REAL ) ; :: thesis: Y = REAL

then for y being object holds

( y in Y iff y in REAL ) ;

hence Y = REAL by TARSKI:2; :: thesis: verum

( r in Y iff r in REAL )

let r be Real; :: thesis: ( r in Y iff r in REAL )

thus ( r in Y implies r in REAL ) ; :: thesis: ( r in REAL implies r in Y )

thus ( r in REAL implies r in Y ) by A1; :: thesis: verum