let A be finite Approximation_Space; 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; 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; ( X c= Y implies (MemberFunc (X,A)) . x <= (MemberFunc (Y,A)) . x )
set CI = Class ( the InternalRel of A,x);
assume
X c= Y
; (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; verum