let A be finite Approximation_Space; :: thesis: for X being Subset of A
for x being Element of A holds
( (MemberFunc X,A) . x = 0 iff x in (UAp X) ` )
let X be Subset of A; :: thesis: for x being Element of A holds
( (MemberFunc X,A) . x = 0 iff x in (UAp X) ` )
let x be Element of A; :: thesis: ( (MemberFunc X,A) . x = 0 iff x in (UAp X) ` )

hereby :: thesis: ( x in (UAp X) ` implies (MemberFunc X,A) . x = 0 )

assume A1: (MemberFunc X,A) . x = 0 ; :: thesis: x in (UAp X) `
(MemberFunc X,A) . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) by Def9;
then X /\ (Class the InternalRel of A,x) = {} by A1, XCMPLX_1:50;
then X misses Class the InternalRel of A,x by XBOOLE_0:def 7;
then not x in UAp X by Th10;
hence x in (UAp X) ` by XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (UAp X) ` ; :: thesis: (MemberFunc X,A) . x = 0
then not x in UAp X by XBOOLE_0:def 5;
then X misses Class the InternalRel of A,x ;
then A2: card (X /\ (Class the InternalRel of A,x)) = 0 by CARD_1:47, XBOOLE_0:def 7;
(MemberFunc X,A) . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) by Def9;
hence (MemberFunc X,A) . x = 0 by A2; :: thesis: verum