let S be RealNormSpace; :: thesis: for Y being Subset of S holds
( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
let Y be Subset of S; :: thesis: ( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
thus ( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) implies Y = the carrier of S ) :: thesis: ( Y = the carrier of S implies for r being Point of S holds
( r in Y iff r in the carrier of S ) )

proof

assume for r being Point of S holds
( r in Y iff r in the carrier of S ) ; :: thesis: Y = the carrier of S
then for y being object holds
( y in Y iff y in the carrier of S ) ;
hence Y = the carrier of S by TARSKI:2; :: thesis: verum

end;

assume A1: Y = the carrier of S ; :: thesis: for r being Point of S holds
( r in Y iff r in the carrier of S )
let r be Point of S; :: thesis: ( r in Y iff r in the carrier of S )
thus ( r in Y implies r in the carrier of S ) ; :: thesis: ( r in the carrier of S implies r in Y )
thus ( r in the carrier of S implies r in Y ) by A1; :: thesis: verum