let A be finite Approximation_Space; :: thesis: for X being Subset of A
for x, y being set st [x,y] in the InternalRel of A holds
(MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
let X be Subset of A; :: thesis: for x, y being set st [x,y] in the InternalRel of A holds
(MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
let x, y be set ; :: thesis: ( [x,y] in the InternalRel of A implies (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y )
assume A1: [x,y] in the InternalRel of A ; :: thesis: (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y
then A2: y is Element of A by ZFMISC_1:87;
x is Element of A by A1, ZFMISC_1:87;
then A3: (MemberFunc (X,A)) . x = (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) by Def9;
x in Class ( the InternalRel of A,y) by A1, EQREL_1:19;
then Class ( the InternalRel of A,x) = Class ( the InternalRel of A,y) by A2, EQREL_1:23;
hence (MemberFunc (X,A)) . x = (MemberFunc (X,A)) . y by A2, A3, Def9; :: thesis: verum