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

( 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

( ( 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 A1:
Y = the carrier of S
; :: thesis: for r being Point of S holds
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;( 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

( 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