let T be non empty right_complementable add-associative right_zeroed RLSStruct ; :: thesis: for B being Subset of T holds (B !) ! = B
let B be Subset of T; :: thesis: (B !) ! = B
thus (B !) ! c= B :: according to XBOOLE_0:def 10 :: thesis: B c= (B !) !

proof

let x be object ; :: 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 Element of T such that
A1: x = - q and
A2: q in B ! ;
ex q1 being Element of T st
( q = - q1 & q1 in B ) by A2;
hence x in B by A1; :: thesis: verum

end;

let x be object ; :: 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 T ;
- xx in { (- q) where q is Point of T : q in B } by A3;
then - (- xx) in { (- q) where q is Point of T : q in B ! } ;
hence x in (B !) ! ; :: thesis: verum