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

hereby :: thesis: ( x in LAp X implies (MemberFunc (X,A)) . x = 1 )

assume A1: (MemberFunc (X,A)) . x = 1 ; :: thesis: x in LAp X
(MemberFunc (X,A)) . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) by Def9;
then card (X /\ (Class ( the InternalRel of A,x))) = card (Class ( the InternalRel of A,x)) by A1, XCMPLX_1:58;
then X /\ (Class ( the InternalRel of A,x)) = Class ( the InternalRel of A,x) by CARD_2:102, XBOOLE_1:17;
then Class ( the InternalRel of A,x) c= X by XBOOLE_1:18;
hence x in LAp X ; :: thesis: verum

end;

assume x in LAp X ; :: thesis: (MemberFunc (X,A)) . x = 1
then A2: card (X /\ (Class ( the InternalRel of A,x))) = card (Class ( the InternalRel of A,x)) by Th8, XBOOLE_1:28;
(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 = 1 by A2, XCMPLX_1:60; :: thesis: verum