let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n) holds 1 (.) X = X
let X be Subset of (TOP-REAL n); :: thesis: 1 (.) X = X
thus 1 (.) X c= X :: according to XBOOLE_0:def 10 :: thesis: X c= 1 (.) X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 1 (.) X or x in X )
assume x in 1 (.) X ; :: thesis: x in X
then ex z being Point of (TOP-REAL n) st
( x = 1 * z & z in X ) ;
hence x in X by RLVECT_1:def 8; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in 1 (.) X )
assume A1: x in X ; :: thesis: x in 1 (.) X
then reconsider x1 = x as Point of (TOP-REAL n) ;
x1 = 1 * x1 by RLVECT_1:def 8;
hence x in 1 (.) X by A1; :: thesis: verum