let A be Approximation_Space; :: thesis: for X being Subset of A holds LAp (LAp X) = LAp X
let X be Subset of A; :: thesis: LAp (LAp X) = LAp X
thus LAp (LAp X) c= LAp X by Th12; :: according to XBOOLE_0:def 10 :: thesis: LAp X c= LAp (LAp X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LAp X or x in LAp (LAp X) )
assume A1: x in LAp X ; :: thesis: x in LAp (LAp X)
then A2: Class ( the InternalRel of A,x) c= X by Th8;
Class ( the InternalRel of A,x) c= LAp X

proof

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

end;

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