let A be Approximation_Space; :: thesis: for X being Subset of A holds LAp (LAp X) = UAp (LAp X)
let X be Subset of A; :: thesis: LAp (LAp X) = UAp (LAp X)
thus LAp (LAp X) c= UAp (LAp X) by Th14; :: according to XBOOLE_0:def 10 :: thesis: UAp (LAp X) c= LAp (LAp X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (LAp X) or x in LAp (LAp X) )
assume A1: x in UAp (LAp X) ; :: thesis: x in LAp (LAp X)
then Class the InternalRel of A,x meets LAp X by Th10;
then consider z being set such that
A2: z in Class the InternalRel of A,x and
A3: z in LAp X by XBOOLE_0:3;
Class the InternalRel of A,z c= X by A3, Th8;
then A4: Class the InternalRel of A,x c= X by A1, A2, EQREL_1:31;
Class the InternalRel of A,x c= LAp X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Class the InternalRel of A,x or y in LAp X )
assume A5: 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:31;
hence y in LAp X by A4, A5; :: thesis: verum

end;

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