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 ) )

proof

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;

assume A1: Y = REAL ; :: thesis: for r being Real holds
( 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