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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp X or y in { x where x is Element of A : (MemberFunc (X,A)) . x > 0 } )
assume A1: y in UAp X ; :: thesis: y in { x where x is Element of A : (MemberFunc (X,A)) . x > 0 }
then reconsider y9 = y as Element of A ;
not y in (UAp X) ` by A1, XBOOLE_0:def 5;
then (MemberFunc (X,A)) . y9 <> 0 by Th41;
then (MemberFunc (X,A)) . y9 > 0 by Th38;
hence y in { x where x is Element of A : (MemberFunc (X,A)) . x > 0 } ; :: 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 > 0 } or y in UAp X )
assume y in { x where x is Element of A : (MemberFunc (X,A)) . x > 0 } ; :: thesis: y in UAp X
then A2: ex y9 being Element of A st
( y9 = y & (MemberFunc (X,A)) . y9 > 0 ) ;
then not y in (UAp X) ` by Th41;
hence y in UAp X by A2, XBOOLE_0:def 5; :: thesis: verum