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:44, 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:74;
(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