let A be Approximation_Space; :: thesis: for X being Subset of A holds UAp (UAp X) = UAp X
let X be Subset of A; :: thesis: UAp (UAp X) = UAp X

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: UAp X c= UAp (UAp X)

let x be object ; :: thesis: ( x in UAp (UAp X) implies x in UAp X )
assume A1: x in UAp (UAp X) ; :: thesis: x in UAp X
then Class ( the InternalRel of A,x) meets UAp X by Th10;
then consider y being object such that
A2: y in Class ( the InternalRel of A,x) and
A3: y in UAp X by XBOOLE_0:3;
A4: Class ( the InternalRel of A,y) = Class ( the InternalRel of A,x) by A1, A2, EQREL_1:23;
Class ( the InternalRel of A,y) meets X by A3, Th10;
hence x in UAp X by A1, A4; :: thesis: verum

end;

thus UAp X c= UAp (UAp X) by Th13; :: thesis: verum