let A be finite Approximation_Space; :: thesis: for X, Y being Subset of A
for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
let X, Y be Subset of A; :: thesis: for x being Element of A st X c= Y holds
(MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
let x be Element of A; :: thesis: ( X c= Y implies (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x )
set CI = Class ( the InternalRel of A,x);
assume X c= Y ; :: thesis: (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x
then card (Y /\ (Class ( the InternalRel of A,x))) >= card (X /\ (Class ( the InternalRel of A,x))) by NAT_1:43, XBOOLE_1:26;
then A1: (card (Y /\ (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 XREAL_1:72;
(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 <= (MemberFunc (Y,A)) . x by A1, Def9; :: thesis: verum