let A be finite Tolerance_Space; :: thesis: for X being Subset of
for x being Element of holds (MemberFunc X,A) . x in [.0 ,1.]
let X be Subset of ; :: thesis: for x being Element of holds (MemberFunc X,A) . x in [.0 ,1.]
let x be Element of ; :: thesis: (MemberFunc X,A) . x in [.0 ,1.]
( 0 <= (MemberFunc X,A) . x & (MemberFunc X,A) . x <= 1 ) by Th38;
hence (MemberFunc X,A) . x in [.0 ,1.] by XXREAL_1:1; :: thesis: verum