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 - ((MemberFunc (X,A)) . x)
let X be Subset of A; :: thesis: for x being Element of A holds (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
let x be Element of A; :: thesis: (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x)
A1: ([#] A) /\ (Class ( the InternalRel of A,x)) = Class ( the InternalRel of A,x) by XBOOLE_1:28;
(MemberFunc ((X `),A)) . x = (card ((([#] A) \ X) /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) by Def9
.= (card ((([#] A) /\ (Class ( the InternalRel of A,x))) \ (X /\ (Class ( the InternalRel of A,x))))) / (card (Class ( the InternalRel of A,x))) by XBOOLE_1:50
.= ((card (([#] A) /\ (Class ( the InternalRel of A,x)))) - (card (X /\ (Class ( the InternalRel of A,x))))) / (card (Class ( the InternalRel of A,x))) by A1, CARD_2:44, XBOOLE_1:17
.= ((card (([#] A) /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))) - ((card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))) by XCMPLX_1:120
.= ((card (Class ( the InternalRel of A,x))) / (card (Class ( the InternalRel of A,x)))) - ((card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))) by XBOOLE_1:28
.= 1 - ((card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x)))) by XCMPLX_1:60
.= 1 - ((MemberFunc (X,A)) . x) by Def9 ;
hence (MemberFunc ((X `),A)) . x = 1 - ((MemberFunc (X,A)) . x) ; :: thesis: verum