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:106;
x is Element of A by A1, ZFMISC_1:106;
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:27;
then Class the InternalRel of A,x = Class the InternalRel of A,y by A2, EQREL_1:31;
hence (MemberFunc X,A) . x = (MemberFunc X,A) . y by A2, A3, Def9; :: thesis: verum