let n be Element of NAT ; :: thesis: for B being Subset of (TOP-REAL n) holds (B ! ) ! = B
let B be Subset of (TOP-REAL n); :: thesis: (B ! ) ! = B
thus (B ! ) ! c= B :: according to XBOOLE_0:def 10 :: thesis: B c= (B ! ) !

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (B ! ) ! or x in B )
assume x in (B ! ) ! ; :: thesis: x in B
then consider q being Point of (TOP-REAL n) such that
A1: x = - q and
A2: q in B ! ;
ex q1 being Point of (TOP-REAL n) st
( q = - q1 & q1 in B ) by A2;
hence x in B by A1, EUCLID:39; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in (B ! ) ! )
assume A3: x in B ; :: thesis: x in (B ! ) !
then reconsider xx = x as Point of (TOP-REAL n) ;
- xx in { (- q) where q is Point of (TOP-REAL n) : q in B } by A3;
then - (- xx) in { (- q) where q is Point of (TOP-REAL n) : q in B ! } ;
hence x in (B ! ) ! by EUCLID:39; :: thesis: verum