let A be finite Tolerance_Space; :: thesis: for X being Subset of A
for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
let X be Subset of A; :: thesis: for x being Element of A holds
( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
let x be Element of A; :: thesis: ( 0 <= (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x <= 1 )
(card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) >= 0 ;
hence 0 <= (MemberFunc (X,A)) . x by Def9; :: thesis: (MemberFunc (X,A)) . x <= 1
card (X /\ (Class ( the InternalRel of A,x))) <= card (Class ( the InternalRel of A,x)) by NAT_1:43, XBOOLE_1:17;
then (card (X /\ (Class ( the InternalRel of A,x)))) / (card (Class ( the InternalRel of A,x))) <= 1 by XREAL_1:185;
hence (MemberFunc (X,A)) . x <= 1 by Def9; :: thesis: verum