let A be finite Tolerance_Space; for X being Subset of A
for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]
let X be Subset of A; for x being Element of A holds (MemberFunc (X,A)) . x in [.0,1.]
let x be Element of A; (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; verum