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