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 & q in B ! ) ;
consider q1 being Point of (TOP-REAL n) such that
A2: ( q = - q1 & q1 in B ) by A1;
x = q1 by A1, A2, EUCLID:39;
hence x in B by A1, A2; :: 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 ! } ;
then xx in { (- q) where q is Point of (TOP-REAL n) : q in B ! } by EUCLID:39;
hence x in (B ! ) ! ; :: thesis: verum