let A be finite Approximation_Space; :: thesis: for X being Subset of A holds LAp X = { x where x is Element of A : (MemberFunc (X,A)) . x = 1 }
let X be Subset of A; :: thesis: LAp X = { x where x is Element of A : (MemberFunc (X,A)) . x = 1 }
thus LAp X c= { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } c= LAp X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in LAp X or y in { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } )
assume A1: y in LAp X ; :: thesis: y in { x where x is Element of A : (MemberFunc (X,A)) . x = 1 }
then reconsider y9 = y as Element of A ;
(MemberFunc (X,A)) . y9 = 1 by A1, Th40;
hence y in { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } or y in LAp X )
assume y in { x where x is Element of A : (MemberFunc (X,A)) . x = 1 } ; :: thesis: y in LAp X
then ex y9 being Element of A st
( y9 = y & (MemberFunc (X,A)) . y9 = 1 ) ;
hence y in LAp X by Th40; :: thesis: verum