let A be Approximation_Space; :: thesis: for X being Subset of A holds UAp (UAp X) = LAp (UAp X)
let X be Subset of A; :: thesis: UAp (UAp X) = LAp (UAp X)
thus UAp (UAp X) c= LAp (UAp X) :: according to XBOOLE_0:def 10 :: thesis: LAp (UAp X) c= UAp (UAp X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (UAp X) or x in LAp (UAp X) )
assume A1: x in UAp (UAp X) ; :: thesis: x in LAp (UAp X)
then Class ( the InternalRel of A,x) meets UAp X by Th10;
then consider z being object such that
A2: z in Class ( the InternalRel of A,x) and
A3: z in UAp X by XBOOLE_0:3;
A4: Class ( the InternalRel of A,z) = Class ( the InternalRel of A,x) by A1, A2, EQREL_1:23;
A5: Class ( the InternalRel of A,z) meets X by A3, Th10;
Class ( the InternalRel of A,x) c= UAp X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Class ( the InternalRel of A,x) or y in UAp X )
assume A6: y in Class ( the InternalRel of A,x) ; :: thesis: y in UAp X
then Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y) by A1, EQREL_1:23;
hence y in UAp X by A5, A4, A6; :: thesis: verum

end;

hence x in LAp (UAp X) by A1; :: thesis: verum

end;

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