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

proof

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

end;

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