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:44, XBOOLE_1:17;
then (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) <= 1 by XREAL_1:187;
hence (MemberFunc X,A) . x <= 1 by Def9; :: thesis: verum